gen_tyvarify : term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Instantiates a term with fresh type variables
DESCRIPTION
A call to gen_tyvarify tm renames all of the type variables in term tm to fresh replacements (generated with gen_tyvar).
FAILURE
Never fails.
EXAMPLE
> show_types := true;
> gen_tyvarify “h::t”;
<<HOL message: inventing new type variable names: 'a>>
val it = “(h :%%gen_tyvar%%30)::(t :%%gen_tyvar%%30 list)”: term
SEEALSO
gen_tyvar
HOL  Trindemossen-1