match_term : term -> term -> (term,term) subst * (hol_type,hol_type) subst
STRUCTURE
Term
SYNOPSIS
Finds instantiations to match one term to another.
DESCRIPTION
An application match_term M N attempts to find a set of type and term instantiations for M to make it alpha-convertible to N. If match_term succeeds, it returns the instantiations in the form of a pair containing a term substitution and a type substitution. In particular, if match_term pat ob succeeds in returning a value (S,T), then 
   aconv (subst S (inst T pat)) ob.

FAILURE
Fails if the term cannot be matched by one-way instantiation.
EXAMPLE
The following shows how match_term could be used to match the conclusion of a theorem to a term. 
   - val th = REFL (Term `x:'a`);
    val th = |- x = x : thm

   - match_term (concl th) (Term `1 = 1`);
   val it = ([{redex = `x`, residue = `1`}],
             [{redex = `:'a`, residue = `:num`}])
     : term subst * hol_type subst

  - INST_TY_TERM it th;
  val it = |- 1 = 1

COMMENTS
For instantiating theorems PART_MATCH is usually easier to use.
SEEALSO
match_terml, match_type, INST_TY_TERM, PART_MATCH
HOL  Kananaskis-11