src/Pure/type.ML
changeset 19806 f860b7a98445
parent 19696 26a268c299d8
child 20071 8f3e1ddb50e6
     1.1 --- a/src/Pure/type.ML	Wed Jun 07 02:01:27 2006 +0200
     1.2 +++ b/src/Pure/type.ML	Wed Jun 07 02:01:28 2006 +0200
     1.3 @@ -40,8 +40,6 @@
     1.4    (*special treatment of type vars*)
     1.5    val strip_sorts: typ -> typ
     1.6    val no_tvars: typ -> typ
     1.7 -  val varifyT: typ -> typ
     1.8 -  val unvarifyT: typ -> typ
     1.9    val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
    1.10    val freeze_thaw_type: typ -> typ * (typ -> typ)
    1.11    val freeze_type: typ -> typ
    1.12 @@ -228,10 +226,7 @@
    1.13        commas_quote (map (Term.string_of_vname o #1) vs), [T], []));
    1.14  
    1.15  
    1.16 -(* varify, unvarify *)
    1.17 -
    1.18 -val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
    1.19 -val unvarifyT = map_type_tvar (fn ((a, 0), S) => TFree (a, S) | v => TVar v);
    1.20 +(* varify *)
    1.21  
    1.22  fun varify (t, fixed) =
    1.23    let