Term unification now symmetric

Given two terms 't1' and 't2' and a number of variables 'nvars' the algorithm finds a substitution for the
variables so that none of the variables occurs in the substitution terms and that the substitution applied
to 't1' and 't2' makes them identical. In case that no substitution exists the algorithm raises 'Not_found'.
This symmetric version of the unification is necessary in order to apply it within the type checker.

Fix: There has been a bug in the function 'sub'. The substitution terms have to be shifted up by 'nb' in case
that the substitution happens in an environment with 'nb' bound variables.

Optimization: The functions 'upbound' and 'up' check if the number of shifts is zero. In this case nothing
has to be done, i.e. the algorithm is applied only to shifts above zero.

	modified:   ocaml/term.ml