GEN_TYVARIFY
Drule.GEN_TYVARIFY : thm -> thm
Replace a theorem's type variables with fresh versions
A call to GEN_TYVARIFY th replaces (with INST_TYPE) the type
variables occurring in theorem th's conclusion that do not also appear
in any of th's hypotheses. The new type variables are generated by
successive calls to gen_tyvar, so should not have been seen before.
Failure
Never fails.
Comments
The derived rule FULL_GEN_TYVARIFY will instantiate all of a theorem's
type variables, whether or not they appear in the hypotheses.
See also
Drule.FULL_GEN_TYVARIFY,
boolSyntax.gen_tyvar_sigma,
Thm.INST_TYPE