src/Pure/type.ML

   val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
 
   (*special treatment of type vars*)
   val strip_sorts: typ -> typ
   val no_tvars: typ -> typ
-  val varifyT: typ -> typ
-  val unvarifyT: typ -> typ
   val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
   val freeze_thaw_type: typ -> typ * (typ -> typ)
   val freeze_type: typ -> typ
   val freeze_thaw: term -> term * (term -> term)
   val freeze: term -> term

   (case typ_tvars T of [] => T
   | vs => raise TYPE ("Illegal schematic type variable(s): " ^
       commas_quote (map (Term.string_of_vname o #1) vs), [T], []));
 
 
-(* varify, unvarify *)
-
-val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
-val unvarifyT = map_type_tvar (fn ((a, 0), S) => TFree (a, S) | v => TVar v);
+(* varify *)
 
 fun varify (t, fixed) =
   let
     val fs = Term.fold_types (Term.fold_atyps
       (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];