Get FullUnify to build under Moscow ML

Remove Unicode in comments in FullUnify.sml

Work towards a general unification module

There is an existing piece of code in src/simp/src, but it doesn't
handle type variables, which I think we want. (That's why I've called
this one FullUnify, because the other module has taken the Unify name,
at least for now.) The functions are parameterized by predicates for
specifying which variables should be treated as unifiable. I'm not
sure what the signature should be just yet, but that for
type-unification is probably right.

The term unification, not yet exposed in the sig, attempts to do a
very brain-dead handling of pattern-like situations when it sees
abstractions. The handling of the fact that terms are typed with
things that are themselves polymorphic is inspired by the code in
Isabelle (term environments are maps from strings to type-term pairs).