----------------------------------------------------------------------
INST_TY_TERM                                                   (Drule)
----------------------------------------------------------------------
INST_TY_TERM :
(term,term)subst * (hol_type,hol_type)subst -> thm -> thm

SYNOPSIS
Instantiates terms and types of a theorem.

KEYWORDS
rule, type, instantiate.

DESCRIBE
{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
Thm.INST, Thm.INST_TYPE, Drule.ISPEC, Thm.SPEC, Drule.SUBS, Thm.SUBST,
Term.norm_subst, Drule.INST_TT_HYPS.

----------------------------------------------------------------------