match : term -> term -> (term * term) list * (hol_type * hol_type) list
Finds 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.

HOL  Kananaskis-14