----------------------------------------------------------------------
match                                                       (hol88Lib)
----------------------------------------------------------------------
match : term -> term -> (term * term) list * (hol_type * hol_type) list

SYNOPSIS
Finds instantiations to match one term to another.

DESCRIBE
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).

Superseded by {Term.match_term}.

SEEALSO
Term.match_term.

----------------------------------------------------------------------