Implemented check for ghostness in functions

If functions have a definition term which contains ghost functions
then the function must be a ghost function.

	modified:   ocaml/feature_table.ml
	modified:   ocaml/signature.ml
Added finding of witnesses for existential quantification

If the prover wants to prove an assertion of the form

    some(a,b,...) p(a,b,...)

it searches for an expression in the context which can be used as
a witness.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli