INST_TY_TERM :
(term,term)subst * (hol_type,hol_type)subst -> thm -> thm
STRUCTURE
SYNOPSIS
Instantiates terms and types of a theorem.
DESCRIPTION
INST_TY_TERM instantiates types in a theorem, in the same way INST_TYPE does. Then it instantiates some or all of the free variables in the resulting theorem, in the same way as INST.
COMMENTS
Because the types are instantiated first, the terms (redexes as well as residues) in the term substitution must contain the substituted types, not the original ones. Use norm_subst to achieve this.
FAILURE
INST_TY_TERM fails under the same conditions as either INST or INST_TYPE fail.
SEEALSO
HOL  Trindemossen-1