Finds instantiations to match one term to another.
DESCRIPTION
When applied to two terms, match_term attempts to find a set of type
and term instantiations for the first term (only) to make it equal the
second. If it succeeds, it returns the instantiations in the form of a
pair containing a hol88 term substitution and a hol88 type
substitution. If the first term represents the conclusion of a
theorem, the returned instantiations are of the appropriate form to be
passed to INST_TY_TERM.
FAILURE
Fails if the term cannot be matched by one-way instantiation.
COMMENTS
Note that INST_TY_TERM may still fail (when a variable that is
instantiated occurs free in the theorem’s assumptions).