First step to make symmetric unification incremental

The substitution consisting of an array of terms and an array of flags has been factored out in
order to make unification incremental.

	modified:   ocaml/term.ml