1\DOC INST_TY_TERM 2 3\BLTYPE 4INST_TY_TERM : 5(term,term)subst * (hol_type,hol_type)subst -> thm -> thm 6\ELTYPE 7 8\SYNOPSIS 9Instantiates terms and types of a theorem. 10 11\KEYWORDS 12rule, type, instantiate. 13 14\DESCRIBE 15{INST_TY_TERM} instantiates types in a theorem, in the same way 16{INST_TYPE} does. Then it instantiates some or all of the free 17variables in the resulting theorem, in the same way as {INST}. 18 19\COMMENTS 20Because the types are instantiated first, the terms (redexes as well as 21residues) in the term substitution must contain the substituted types, not the 22original ones. Use {norm_subst} to achieve this. 23 24\FAILURE 25{INST_TY_TERM} fails under the same conditions as either {INST} or 26{INST_TYPE} fail. 27 28\SEEALSO 29Thm.INST, Thm.INST_TYPE, Drule.ISPEC, Thm.SPEC, Drule.SUBS, Thm.SUBST, 30Term.norm_subst, Drule.INST_TT_HYPS 31\ENDDOC 32