# HG changeset patch
# User paulson
# Date 865511729 -7200
# Node ID 163f8f4a42d7c8f6c48220d5d9312fc242e19ea8
# Parent  98f59f455d57be2a7957c423b2c7380c6831c842
Removal of freeze_vars and thaw_vars.  New freeze_thaw

diff -r 98f59f455d57 -r 163f8f4a42d7 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Jun 05 13:53:59 1997 +0200
+++ b/src/Pure/type.ML	Thu Jun 05 13:55:29 1997 +0200
@@ -12,9 +12,7 @@
   val varifyT: typ -> typ
   val unvarifyT: typ -> typ
   val varify: term * string list -> term
-  val freeze_vars: typ -> typ
-  val thaw_vars: typ -> typ
-  val freeze: term -> term
+  val freeze_thaw : term -> term * (term -> term)
 
   (*type signatures*)
   type type_sig
@@ -105,60 +103,37 @@
   end;
 
 
-(* thaw, freeze *)
+(** Freeze TVars in a term; return the "thaw" inverse **)
+
+fun newName (ix, (pairs,used)) = 
+      let val v = variant used (string_of_indexname ix)
+      in  ((ix,v)::pairs, v::used)  end;
 
-val thaw_vars =
-  let
-    fun thaw (f as (a, S)) =
-      (case explode a of
-        "?" :: "'" :: vn =>
-          let val ((b, i), _) = Syntax.scan_varname vn in
-            TVar (("'" ^ b, i), S)
-          end
-      | _ => TFree f)
-  in map_type_tfree thaw end;
+fun freezeOne alist (ix,sort) = TFree (the (assoc (alist, ix)), sort)
+      handle OPTION _ => 
+	  raise_type ("Failure during freezing of ?" ^
+		      string_of_indexname ix) [] [];
 
-val freeze_vars =
-  map_type_tvar (fn (v, S) => TFree (Syntax.string_of_vname v, S));
-
-
-local
-  fun nextname (pref, c) =
-    if c = "z" then (pref ^ "a", "a")
-    else (pref, chr (ord c + 1));
+fun thawOne alist (a,sort) = TVar (the (assoc (alist,a)), sort)
+      handle OPTION _ => TFree(a,sort);
 
-  fun newtvars used =
-    let
-      fun new ([], _, vmap) = vmap
-        | new (ixn :: ixns, p as (pref, c), vmap) =
-            let val nm = pref ^ c in
-              if nm mem_string used then new (ixn :: ixns, nextname p, vmap)
-              else new (ixns, nextname p, (ixn, nm) :: vmap)
-            end
-    in new end;
-
-  (*Turn all TVars which satisfy p into new (if freeze then TFrees else TVars).
-    Note that if t contains frozen TVars there is the possibility that a TVar is
-    turned into one of those. This is sound but not complete.*)
+(*This sort of code could replace unvarifyT (?)
+    fun freeze_thaw_type T =
+	let val used = add_typ_tfree_names (T, [])
+	  and tvars = map #1 (add_typ_tvars (T, []))
+	  val (alist, _) = foldr newName (tvars, ([], used))
+	in  (map_type_tvar (freezeOne alist) T, 
+	   map_type_tfree (thawOne (map swap alist)))  
+	end;
+*)
 
-  fun convert used freeze p t =
-    let
-      val used =
-        if freeze then add_term_tfree_names (t, used)
-        else used union (map #1 (filter_out p (add_term_tvar_ixns (t, []))));
-      val ixns = filter p (add_term_tvar_ixns (t, []));
-      val vmap = newtvars used (ixns, ("'", "a"), []);
-      fun conv (var as (ixn, S)) =
-        (case assoc (vmap, ixn) of
-          None => TVar(var)
-        | Some a => if freeze then TFree (a, S) else TVar ((a, 0), S));
-    in
-      map_term_types (map_type_tvar conv) t
+fun freeze_thaw t =
+    let val used = it_term_types add_typ_tfree_names (t, [])
+	and tvars = map #1 (it_term_types add_typ_tvars (t, []))
+	val (alist, _) = foldr newName (tvars, ([], used))
+    in  (map_term_types (map_type_tvar (freezeOne alist)) t,
+	 map_term_types (map_type_tfree (thawOne (map swap alist)))) 
     end;
-in
-  fun freeze t = convert (add_term_tfree_names(t,[])) true (K true) t;
-end;
-
 
 
 (*** type signatures ***)