INST_TT_HYPS
Drule.INST_TT_HYPS :
(term,term)subst * (hol_type,hol_type)subst -> thm -> thm * term list
Instantiates terms and types of a theorem.
INST_TT_HYPS instantiates types and terms in a theorem thm, in the
same way INST_TY_TERM does. It also returns a list of the instantiated
hypotheses, in the same order as the uninstantiated hypotheses appear in
the list hyp thm.
Failure
INST_TT_HYPS fails under the same conditions as INST_TY_TERM.