Clean up and added some code to calculate and argument array from a substitution

	modified:   ocaml/term.ml
Reformatted statistics output

	modified:   ocaml/support.ml
Integrated experimental assertion context into assertion table

The unifier still has to be optimized.

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/proof.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/term_table.ml
	modified:   ocaml/term_table.mli
Improved the unifier

If the unifier tries to unify a term which has either a bound variable or a
free variable at a certain position it has access to a map which returns given
the variable directly all assertions (by their indices) which match. No searching
is neccessary.

This improvement speeds up the unifier but slows down to retrieve an assertion
given its index. However the latter operation is practically not needed.

	modified:   ocaml/term_table.ml
Separated out the assertion context into an own module

	new file:   ocaml/assertion_context.ml
	new file:   ocaml/assertion_context.mli
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/term.ml
Splitted out the proof context into an own module

	modified:   ocaml/proof.ml
	new file:   ocaml/proof_context.ml
	new file:   ocaml/proof_context.mli
	modified:   ocaml/prover.ml