Variable names introduced into lambda abstractions

In order to avoid anonymous variable names in lambda abstractions the
variable names have been introduced in lambda abstractions.

Note: The variable types can be recovered from the pure term, but the
variable names not. Therefore it makes sense to include them into the
terms. The names are used only for printouts in order to give the user
the terms how they appear in the source code. The algorithms do not
use the names.

	modified:   ocaml/class_table.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/proof.ml
	modified:   ocaml/term.ml
	modified:   ocaml/term_table0.ml
Minor adaptions

Added a the stub function 'unify_with' and rearranged some argument
lists.

	modified:   ocaml/term_table0.ml
	modified:   ocaml/term_table0.mli
Removed data from the base version of the term table

Removed 'count' and 'nbenv' from 'term_table0.ml'. These data are
stored in the users of the term table and the necessary data are
provided via arguments lists.

	modified:   ocaml/term_table.ml
	modified:   ocaml/term_table0.ml
	modified:   ocaml/term_table0.mli
Added quantifier expressions and more robust code

- Added 'quantified' and 'quantifier_split'

- Binary and unary split run into an 'assert false' if the expression
  is not of the appropriate arity.

	modified:   ocaml/term.ml
Removed unnecessary exception handling

The unifyer of 'term_table0.ml' returns a list of terms which can
be unified with the term under consideration. If no term in the
table can be unified with the term under consideration then the
returned list is empty. Therefore no exception 'Not_found' is
necessary.

	modified:   ocaml/term_table0.ml
Added 'is_empty' to the term substitutions

	modified:   ocaml/term.ml