# HG changeset patch
# User wenzelm
# Date 974573314 -3600
# Node ID 284ee538991c9a3eb0eeab77aecb4a2ed158d86b
# Parent  305b37c8d8a3662436ce9c877475790242994d38
export freeze_thaw_type;

diff -r 305b37c8d8a3 -r 284ee538991c src/Pure/type.ML
--- 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, [])