Fix: Replace term levels by node count of expanded term

The algorithm to break infinite loops with term levels does not work.
With the term level algorithm an expression has been considered as
not more complicated than another if it has not more nodes and not
a higher term level.

However a term might be more complicated as another if it has one more
expandable function than the other but the other term already contains
a function with the same level. Therefore the term level does not grow
but the expanded term might be more complex than the expansion of the
other.

Therefore we use the node count of the fully expanded term as a complexity
measure.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/prover.ml
Fix: An interface file which does not exist cannot be affected

	modified:   ocaml/alba.ml
Fix: Type variables 'Tvars' have to be checked for equivalence

The names of the formal generics are irrelevant. Therefore a function
have been introduced which checks the equivalence of two 'Tvars' and
returns true if everything except the names of the formal generics
is equal.

	modified:   ocaml/feature_table.ml
	modified:   ocaml/tvars.ml
	modified:   ocaml/tvars.mli
Added some functions

	modified:   ocaml/container.ml
	modified:   ocaml/term.ml
Added 'ANY.eq' and 'PREDICATE.()' as basic functions

This required that the feature map in the feature table has to
use a wrapper of the term table (now called 'Term_table2') like
already used in the class table. Reason: It is no longer guaranteed
that the features arrive in ascending sequence. E.g. by the time
of the definition of the function ANY.= in the source file there
are already features with higher index than the builtin index of
the equality function of ANY.

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/feature_table.ml
	new file:   ocaml/term_table2.ml
	new file:   ocaml/term_table2.mli
Used 'error_info' in the parser to raise an error

	modified:   ocaml/parser.mly