match_type : hol_type -> hol_type -> (hol_type,hol_type) subst
STRUCTURE
Type
SYNOPSIS
Calculates a substitution theta such that instantiating the first argument with theta equals the second argument.
DESCRIPTION
If match_type ty1 ty2 succeeds, then 
    type_subst (match_type ty1 ty2) ty1 = ty2

FAILURE
If no such substitution can be found.
EXAMPLE
- match_type alpha (Type`:num`);
> val it = [{redex = `:'a`, residue = `:num`}] : hol_type subst

- let val patt = Type`:('a -> bool) -> 'b`
      val ty =   Type`:(num -> bool) -> bool`
  in
     type_subst (match_type patt ty) patt = ty
  end;
> val it = true : bool

- match_type (alpha --> alpha)
             (ind   --> bool);
! Uncaught exception:
! HOL_ERR
SEEALSO
match_term, type_subst
HOL  Kananaskis-14