gen_tyvarify

boolSyntax.gen_tyvarify : term -> term

Instantiates a term with fresh type variables

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”;
val it = (): unit
val it = “(h :%%gen_tyvar%%35)::(t :%%gen_tyvar%%35 list)”: term

See also

Type.gen_tyvar