term_unify : term list -> term -> term -> instantiation

SYNOPSIS: Unify two terms.
DESCRIPTION: Given two terms tm1 and tm2, a call term_unify vars tm1 tm2 attempts to find instantiations of the variables vars in the two terms to make them alpha-equivalent. At present, no type instantiation is done. The unification is also purely first-order. In these respects it is less general than term_match, and this may be improved in the future.
FAILURE CONDITIONS: Fails if the two terms are not first-order unifiable by instantiating the given variables without type instantiation.
SEE ALSO: instantiate, term_match.