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