INST_TYPE : (hol_type,hol_type) subst -> thm -> thm
STRUCTURE
Thm
SYNOPSIS
Instantiates types in a theorem.
DESCRIPTION
INST_TYPE is a primitive rule in the HOL logic, which allows instantiation of type variables. 

              A |- t
  ----------------------------------- INST_TYPE[vty1|->ty1,..., vtyn|->tyn]
   A[ty1,...,tyn/vty1,...,vtyn]
    |-
   t[ty1,...,tyn/vty1,...,vtyn]
Type substitution is performed throughout the hypotheses and the conclusion. Variables will be renamed if necessary to prevent distinct bound variables becoming identical after the instantiation.
FAILURE
Never fails.
USES
INST_TYPE enables polymorphic theorems to be used at any type.
EXAMPLE
Supposing one wanted to specialize the theorem EQ_SYM_EQ for particular values, the first attempt could be to use SPECL as follows: 
   - SPECL [``a:num``, ``b:num``] EQ_SYM_EQ;
   uncaught exception HOL_ERR
The failure occurred because EQ_SYM_EQ contains polymorphic types. The desired specialization can be obtained by using INST_TYPE: 
   - load "numTheory";

   - SPECL [Term `a:num`, Term`b:num`]
           (INST_TYPE [alpha |-> Type`:num`] EQ_SYM_EQ);

   > val it = |- (a = b) = (b = a) : thm

SEEALSO
inst, INST, INST_TY_TERM, |->
HOL  Trindemossen-1