FULL_GEN_TYVARIFY

Drule.FULL_GEN_TYVARIFY : thm -> thm

Replace a theorem’s type variables with fresh versions

A call to FULL_GEN_TYVARIFTY th replaces (with INST_TYPE) the type variables occurring in theorem th. 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 GEN_TYVARIFY will only instantiate those type variables that are exclusively found in the conclusion. This is reasonable when handling theorems derived from a tactic goal’s assumptions.

See also

Drule.GEN_TYVARIFY, Thm.INST_TYPE