Improved printing functions for signatures

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/signature.ml
	modified:   ocaml/term_builder.ml
	modified:   ocaml/typer.ml
Removed old unnecessary recursion

	modified:   ocaml/typer.ml
Fix: sequence of type variable substitutions

The type introduces new type variables into the type context in two ways:

- If it expects a function it puts a new conceptless type variable at the
  bottom of the type variables for each argument of the function

- If global functions are encountered which are generic it puts new type
  variables with concepts at the top of the type variables

Usually newer type variables get substituted by older. This is always the case
for conceptless type variables because they get a substitution before new
conceptless type variables are introduced.

It is not always the case for type variables with concepts. The default order
might be reversed if the concept of the older is satisfied by the concept of
the newer and not vice versa. Then the older will be substituted by the newer.

	modified:   ocaml/signature.ml
	modified:   ocaml/term_builder.ml
Fix: trace of failed proof did not show up correctly

If a proof fails it is replayed with the trace flag set. In order to
show the same behaviour it has to start with an identical proof environment.

	modified:   prover.ml