raw_match_type 
  : hol_type list 
       -> hol_type -> hol_type
       -> (hol_type,hol_type) subst * hol_type list
       -> (hol_type,hol_type) subst * hol_type list
STRUCTURE
Type
SYNOPSIS
Primitive type matching algorithm.
DESCRIPTION
An invocation raw_match_type away pat ty (S,Id) performs matching, just as match_tyl, except that it takes an extra accumulating parameter (S,Id), which represents a ’raw’ substitution that the match (theta,id) of pat and ty must be compatible with. If matching is successful, (theta,id) is merged with (S,Id) to yield the result.
FAILURE
A call to raw_match_type away pat ty (S,Id) will fail when match_typel away pat ty would. It will also fail when a {redex,residue} calculated in the course of matching pat and ty is such that there is a {redex_i,residue_i} in S and redex equals redex_i but residue does not equal residue_i.
EXAMPLE
- val res1 = raw_match_type [] alpha  (alpha --> bool) ([],[]);
> val it = ([{redex = `:'a`, residue = `:'a -> bool`}], []) : ...

- raw_match_type [] (alpha --> beta --> gamma)
                    ((alpha --> bool) --> beta --> ind) res1;
> val it =([{redex = `:'c`, residue = `:ind`},
            {redex = `:'a`, residue = `:'a -> bool`}], [`:'b`]) : ....

COMMENTS
Probably exposes too much internal state of the matching algorithm.
SEEALSO
match_type, match_typel
HOL  Kananaskis-8