matchhol88Lib.match : term -> term -> (term * term) list * (hol_type * hol_type) listFinds instantiations to match one term to another.
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.
Fails if the term cannot be matched by one-way instantiation.
Note that INST_TY_TERM may still fail (when a variable
that is instantiated occurs free in the theorem’s assumptions).
Superseded by Term.match_term.