# HG changeset patch
# User wenzelm
# Date 1118005647 -7200
# Node ID 9582078159311b69d830fa23ada666a326aafce7
# Parent  df2b550a17f6e312fbebd58473b2a9d2ffd27a42
added Type.freeze(_type);
tuned;

diff -r df2b550a17f6 -r 958207815931 src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Jun 05 23:07:26 2005 +0200
+++ b/src/Pure/type.ML	Sun Jun 05 23:07:27 2005 +0200
@@ -42,8 +42,10 @@
   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_thaw : term -> term * (term -> term)
+  val freeze_thaw_type: typ -> typ * (typ -> typ)
+  val freeze_type: typ -> typ
+  val freeze_thaw: term -> term * (term -> term)
+  val freeze: term -> term
 
   (*matching and unification*)
   exception TYPE_MATCH
@@ -147,7 +149,7 @@
 local
 
 fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
-  | inst_typ env (T as TFree (x, _)) = getOpt (Library.assoc_string (env, x),T)
+  | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
   | inst_typ _ T = T;
 
 fun certify_typ normalize syntax tsig ty =
@@ -233,17 +235,17 @@
 
 local
 
-fun new_name (ix, (pairs,used)) =
-      let val v = variant used (string_of_indexname ix)
-      in  ((ix,v)::pairs, v::used)  end;
+fun new_name (ix, (pairs, used)) =
+  let val v = variant used (string_of_indexname ix)
+  in ((ix, v) :: pairs, v :: used) end;
 
-fun freeze_one alist (ix,sort) =
-  TFree (valOf (assoc (alist, ix)), sort)
+fun freeze_one alist (ix, sort) =
+  TFree (the (assoc_string_int (alist, ix)), sort)
     handle Option =>
       raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
 
-fun thaw_one alist (a,sort) = TVar (valOf (assoc (alist,a)), sort)
-  handle Option => TFree(a, sort);
+fun thaw_one alist (a, sort) = TVar (the (assoc_string (alist, a)), sort)
+  handle Option => TFree (a, sort);
 
 in
 
@@ -255,6 +257,8 @@
     val (alist, _) = foldr new_name ([], used) tvars;
   in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
 
+val freeze_type = #1 o freeze_thaw_type;
+
 fun freeze_thaw t =
   let
     val used = it_term_types add_typ_tfree_names (t, [])
@@ -267,6 +271,8 @@
       map_term_types (map_type_tfree (thaw_one (map swap alist)))))
   end;
 
+val freeze = #1 o freeze_thaw;
+
 end;
 
 
@@ -279,9 +285,11 @@
   quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
   [TVar (ixn, S), TVar (ixn, S')], []);
 
-fun lookup (tye, (ixn, S)) = case Vartab.lookup (tye, ixn) of
+fun lookup (tye, (ixn, S)) =
+  (case Vartab.lookup (tye, ixn) of
     NONE => NONE
-  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S';
+  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
+
 
 (* matching *)
 
@@ -528,7 +536,7 @@
     SOME (decl', _) => err_in_decls c decl decl'
   | NONE => Symtab.update ((c, (decl, stamp ())), types));
 
-fun the_decl types c = fst (valOf (Symtab.lookup (types, c)));
+fun the_decl types c = fst (the (Symtab.lookup (types, c)));
 
 fun change_types f = change_tsig (fn (classes, default, types, arities) =>
   (classes, default, f types, arities));