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.