--- a/src/Pure/type.ML Sat Nov 18 19:48:07 2000 +0100
+++ b/src/Pure/type.ML Sat Nov 18 19:48:34 2000 +0100
@@ -12,6 +12,7 @@
val varifyT: typ -> typ
val unvarifyT: typ -> typ
val varify: term * string list -> term
+ val freeze_thaw_type : typ -> typ * (typ -> typ)
val freeze_thaw : term -> term * (term -> term)
(*type signatures*)
@@ -123,7 +124,9 @@
fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
handle OPTION => TFree(a,sort);
-(*this sort of code could replace unvarifyT (?) -- currently unused*)
+in
+
+(*this sort of code could replace unvarifyT*)
fun freeze_thaw_type T =
let
val used = add_typ_tfree_names (T, [])
@@ -131,8 +134,6 @@
val (alist, _) = foldr new_name (tvars, ([], used));
in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
-in
-
fun freeze_thaw t =
let
val used = it_term_types add_typ_tfree_names (t, [])