# HG changeset patch
# User wenzelm
# Date 1309986719 -7200
# Node ID 93dcfcf914848dea333e530761dd616c2c5c1744
# Parent  b46f5d2d42cc8e24c00ca0b020d57fd4a4023363# Parent  5c9160f420d5c29a482de0d3bec6271f8cddb721
merged

diff -r b46f5d2d42cc -r 93dcfcf91484 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/HOL/Tools/record.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -9,9 +9,9 @@
 
 signature RECORD =
 sig
-  val print_type_abbr: bool Unsynchronized.ref
-  val print_type_as_fields: bool Unsynchronized.ref
-  val timing: bool Unsynchronized.ref
+  val type_abbr: bool Config.T
+  val type_as_fields: bool Config.T
+  val timing: bool Config.T
 
   type info =
    {args: (string * sort) list,
@@ -256,9 +256,9 @@
 
 (* timing *)
 
-val timing = Unsynchronized.ref false;
-fun timeit_msg s x = if ! timing then (warning s; timeit x) else x ();
-fun timing_msg s = if ! timing then warning s else ();
+val timing = Attrib.setup_config_bool @{binding record_timing} (K false);
+fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();
+fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();
 
 
 (* syntax *)
@@ -670,6 +670,15 @@
 
 local
 
+fun split_args (field :: fields) ((name, arg) :: fargs) =
+      if can (unsuffix name) field then
+        let val (args, rest) = split_args fields fargs
+        in (arg :: args, rest) end
+      else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
+  | split_args [] (fargs as (_ :: _)) = ([], fargs)
+  | split_args (_ :: _) [] = raise Fail "expecting more fields"
+  | split_args _ _ = ([], []);
+
 fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
       (name, arg)
   | field_type_tr t = raise TERM ("field_type_tr", [t]);
@@ -683,15 +692,6 @@
     val thy = Proof_Context.theory_of ctxt;
     fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
 
-    fun split_args (field :: fields) ((name, arg) :: fargs) =
-          if can (unsuffix name) field then
-            let val (args, rest) = split_args fields fargs
-            in (arg :: args, rest) end
-          else err ("expecting field " ^ field ^ " but got " ^ name)
-      | split_args [] (fargs as (_ :: _)) = ([], fargs)
-      | split_args (_ :: _) [] = err "expecting more fields"
-      | split_args _ _ = ([], []);
-
     fun mk_ext (fargs as (name, _) :: _) =
           (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
             SOME (ext, alphas) =>
@@ -700,7 +700,8 @@
                   let
                     val (fields', _) = split_last fields;
                     val types = map snd fields';
-                    val (args, rest) = split_args (map fst fields') fargs;
+                    val (args, rest) = split_args (map fst fields') fargs
+                      handle Fail msg => err msg;
                     val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
                     val midx = fold Term.maxidx_typ argtypes 0;
                     val varifyT = varifyT midx;
@@ -717,8 +718,8 @@
                     list_comb
                       (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
                   end
-              | NONE => err ("no fields defined for " ^ ext))
-          | NONE => err (name ^ " is no proper field"))
+              | NONE => err ("no fields defined for " ^ quote ext))
+          | NONE => err (quote name ^ " is no proper field"))
       | mk_ext [] = more;
   in
     mk_ext (field_types_tr t)
@@ -742,27 +743,18 @@
     val thy = Proof_Context.theory_of ctxt;
     fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
 
-    fun split_args (field :: fields) ((name, arg) :: fargs) =
-          if can (unsuffix name) field
-          then
-            let val (args, rest) = split_args fields fargs
-            in (arg :: args, rest) end
-          else err ("expecting field " ^ field ^ " but got " ^ name)
-      | split_args [] (fargs as (_ :: _)) = ([], fargs)
-      | split_args (_ :: _) [] = err "expecting more fields"
-      | split_args _ _ = ([], []);
-
     fun mk_ext (fargs as (name, _) :: _) =
           (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
             SOME (ext, _) =>
               (case get_extfields thy ext of
                 SOME fields =>
                   let
-                    val (args, rest) = split_args (map fst (fst (split_last fields))) fargs;
+                    val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
+                      handle Fail msg => err msg;
                     val more' = mk_ext rest;
                   in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
-              | NONE => err ("no fields defined for " ^ ext))
-          | NONE => err (name ^ " is no proper field"))
+              | NONE => err ("no fields defined for " ^ quote ext))
+          | NONE => err (quote name ^ " is no proper field"))
       | mk_ext [] = more;
   in mk_ext (fields_tr t) end;
 
@@ -774,7 +766,7 @@
 
 
 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
-      Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
+      Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
   | field_update_tr t = raise TERM ("field_update_tr", [t]);
 
 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
@@ -800,8 +792,8 @@
 
 (* print translations *)
 
-val print_type_abbr = Unsynchronized.ref true;
-val print_type_as_fields = Unsynchronized.ref true;
+val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
+val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);
 
 
 local
@@ -850,7 +842,7 @@
       foldr1 field_types_tr'
         (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
   in
-    if not (! print_type_as_fields) orelse null fields then raise Match
+    if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
     else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
     else
       Syntax.const @{syntax_const "_record_type_scheme"} $ u $
@@ -872,7 +864,7 @@
 
     fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   in
-    if ! print_type_abbr then
+    if Config.get ctxt type_abbr then
       (case last_extT T of
         SOME (name, _) =>
           if name = last_ext then
@@ -1377,7 +1369,7 @@
                             @{const_name all} => all_thm
                           | @{const_name All} => All_thm RS eq_reflection
                           | @{const_name Ex} => Ex_thm RS eq_reflection
-                          | _ => error "split_simproc"))
+                          | _ => raise Fail "split_simproc"))
                   else NONE
                 end)
           else NONE
@@ -1579,6 +1571,8 @@
 
 fun extension_definition name fields alphas zeta moreT more vars thy =
   let
+    val ctxt = Proof_Context.init_global thy;
+
     val base_name = Long_Name.base_name name;
 
     val fieldTs = map snd fields;
@@ -1629,14 +1623,14 @@
           in (term, thy') end
       end;
 
-    val _ = timing_msg "record extension preparing definitions";
+    val _ = timing_msg ctxt "record extension preparing definitions";
 
 
     (* 1st stage part 1: introduce the tree of new types *)
 
     fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
     val (ext_body, typ_thy) =
-      timeit_msg "record extension nested type def:" get_meta_tree;
+      timeit_msg ctxt "record extension nested type def:" get_meta_tree;
 
 
     (* prepare declarations and definitions *)
@@ -1652,19 +1646,19 @@
       |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
       ||> Theory.checkpoint
     val ([ext_def], defs_thy) =
-      timeit_msg "record extension constructor def:" mk_defs;
+      timeit_msg ctxt "record extension constructor def:" mk_defs;
 
 
     (* prepare propositions *)
 
-    val _ = timing_msg "record extension preparing propositions";
+    val _ = timing_msg ctxt "record extension preparing propositions";
     val vars_more = vars @ [more];
     val variants = map (fn Free (x, _) => x) vars_more;
     val ext = mk_ext vars_more;
     val s = Free (rN, extT);
     val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
 
-    val inject_prop =
+    val inject_prop =  (* FIXME local x x' *)
       let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
         HOLogic.mk_conj (HOLogic.eq_const extT $
           mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
@@ -1676,7 +1670,7 @@
     val induct_prop =
       (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
 
-    val split_meta_prop =
+    val split_meta_prop =  (* FIXME local P *)
       let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
         Logic.mk_equals
          (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
@@ -1694,7 +1688,7 @@
                 Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
                 rtac refl 1)));
 
-    val inject = timeit_msg "record extension inject proof:" inject_prf;
+    val inject = timeit_msg ctxt "record extension inject proof:" inject_prf;
 
     (*We need a surjection property r = (| f = f r, g = g r ... |)
       to prove other theorems. We haven't given names to the accessors
@@ -1716,7 +1710,7 @@
       in
         surject
       end;
-    val surject = timeit_msg "record extension surjective proof:" surject_prf;
+    val surject = timeit_msg ctxt "record extension surjective proof:" surject_prf;
 
     fun split_meta_prf () =
       prove_standard [] split_meta_prop
@@ -1726,7 +1720,7 @@
             etac meta_allE, atac,
             rtac (prop_subst OF [surject]),
             REPEAT o etac meta_allE, atac]);
-    val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
+    val split_meta = timeit_msg ctxt "record extension split_meta proof:" split_meta_prf;
 
     fun induct_prf () =
       let val (assm, concl) = induct_prop in
@@ -1736,7 +1730,7 @@
             resolve_tac prems 2 THEN
             asm_simp_tac HOL_ss 1)
       end;
-    val induct = timeit_msg "record extension induct proof:" induct_prf;
+    val induct = timeit_msg ctxt "record extension induct proof:" induct_prf;
 
     val ([induct', inject', surjective', split_meta'], thm_thy) =
       defs_thy
@@ -1797,6 +1791,7 @@
 
 fun mk_random_eq tyco vs extN Ts =
   let
+    (* FIXME local i etc. *)
     val size = @{term "i::code_numeral"};
     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
     val T = Type (tyco, map TFree vs);
@@ -1816,23 +1811,25 @@
 
 fun mk_full_exhaustive_eq tyco vs extN Ts =
   let
+    (* FIXME local i etc. *)
     val size = @{term "i::code_numeral"};
     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
     val T = Type (tyco, map TFree vs);
     val test_function = Free ("f", termifyT T --> @{typ "term list option"});
     val params = Name.invent_names Name.context "x" Ts;
-    fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
-      --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+    fun full_exhaustiveT T =
+      (termifyT T --> @{typ "Code_Evaluation.term list option"}) -->
+        @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"};
     fun mk_full_exhaustive T =
       Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
-        full_exhaustiveT T)
+        full_exhaustiveT T);
     val lhs = mk_full_exhaustive T $ test_function $ size;
     val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
     val rhs = fold_rev (fn (v, T) => fn cont =>
-        mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc
+        mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
   in
     (lhs, rhs)
-  end
+  end;
 
 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
   let
@@ -1844,7 +1841,7 @@
     |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
     |> snd
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
-  end
+  end;
 
 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
   let
@@ -1877,8 +1874,9 @@
       |> Thm.instantiate
         ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
       |> AxClass.unoverload thy;
-    val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq)
-    val ensure_exhaustive_record = ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq)
+    val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
+    val ensure_exhaustive_record =
+      ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
   in
     thy
     |> Code.add_datatype [ext]
@@ -1902,6 +1900,8 @@
 
 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
   let
+    val ctxt = Proof_Context.init_global thy;
+
     val prefix = Binding.name_of binding;
     val name = Sign.full_name thy binding;
     val full = Sign.full_name_path thy prefix;
@@ -1959,7 +1959,7 @@
       |> Sign.qualified_path false binding
       |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
 
-    val _ = timing_msg "record preparing definitions";
+    val _ = timing_msg ctxt "record preparing definitions";
     val Type extension_scheme = extT;
     val extension_name = unsuffix ext_typeN (fst extension_scheme);
     val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
@@ -2063,7 +2063,7 @@
          updaccs RL [updacc_cong_from_eq])
       end;
     val (accessor_thms, updator_thms, upd_acc_cong_assists) =
-      timeit_msg "record getting tree access/updates:" get_access_update_thms;
+      timeit_msg ctxt "record getting tree access/updates:" get_access_update_thms;
 
     fun lastN xs = drop parent_fields_len xs;
 
@@ -2129,11 +2129,11 @@
         [make_spec, fields_spec, extend_spec, truncate_spec]
       ||> Theory.checkpoint
     val (((sel_defs, upd_defs), derived_defs), defs_thy) =
-      timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
+      timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
         mk_defs;
 
     (* prepare propositions *)
-    val _ = timing_msg "record preparing propositions";
+    val _ = timing_msg ctxt "record preparing propositions";
     val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
     val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
     val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
@@ -2213,17 +2213,17 @@
 
     fun sel_convs_prf () =
       map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
-    val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
+    val sel_convs = timeit_msg ctxt "record sel_convs proof:" sel_convs_prf;
     fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
     val sel_convs_standard =
-      timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
+      timeit_msg ctxt "record sel_convs_standard proof:" sel_convs_standard_prf;
 
     fun upd_convs_prf () =
       map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
-    val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
+    val upd_convs = timeit_msg ctxt "record upd_convs proof:" upd_convs_prf;
     fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
     val upd_convs_standard =
-      timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
+      timeit_msg ctxt "record upd_convs_standard proof:" upd_convs_standard_prf;
 
     fun get_upd_acc_congs () =
       let
@@ -2232,7 +2232,7 @@
         val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
       in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
     val (fold_congs, unfold_congs) =
-      timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
+      timeit_msg ctxt "record upd fold/unfold congs:" get_upd_acc_congs;
 
     val parent_induct = Option.map #induct_scheme (try List.last parents);
 
@@ -2243,7 +2243,7 @@
            [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
             try_param_tac rN ext_induct 1,
             asm_simp_tac HOL_basic_ss 1]);
-    val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
+    val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" induct_scheme_prf;
 
     fun induct_prf () =
       let val (assm, concl) = induct_prop in
@@ -2252,7 +2252,7 @@
           THEN try_param_tac "more" @{thm unit.induct} 1
           THEN resolve_tac prems 1)
       end;
-    val induct = timeit_msg "record induct proof:" induct_prf;
+    val induct = timeit_msg ctxt "record induct proof:" induct_prf;
 
     fun cases_scheme_prf () =
       let
@@ -2265,14 +2265,14 @@
         in Object_Logic.rulify (mp OF [ind, refl]) end;
 
     val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
-    val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
+    val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" cases_scheme_prf;
 
     fun cases_prf () =
       prove_standard [] cases_prop
         (fn _ =>
           try_param_tac rN cases_scheme 1 THEN
           simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
-    val cases = timeit_msg "record cases proof:" cases_prf;
+    val cases = timeit_msg ctxt "record cases proof:" cases_prf;
 
     fun surjective_prf () =
       let
@@ -2288,7 +2288,7 @@
                 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
                   (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
       end;
-    val surjective = timeit_msg "record surjective proof:" surjective_prf;
+    val surjective = timeit_msg ctxt "record surjective proof:" surjective_prf;
 
     fun split_meta_prf () =
       prove false [] split_meta_prop
@@ -2298,10 +2298,10 @@
             etac meta_allE, atac,
             rtac (prop_subst OF [surjective]),
             REPEAT o etac meta_allE, atac]);
-    val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
+    val split_meta = timeit_msg ctxt "record split_meta proof:" split_meta_prf;
     fun split_meta_standardise () = Drule.export_without_context split_meta;
     val split_meta_standard =
-      timeit_msg "record split_meta standard:" split_meta_standardise;
+      timeit_msg ctxt "record split_meta standard:" split_meta_standardise;
 
     fun split_object_prf () =
       let
@@ -2328,7 +2328,7 @@
 
 
     val split_object_prf = future_forward_prf split_object_prf split_object_prop;
-    val split_object = timeit_msg "record split_object proof:" split_object_prf;
+    val split_object = timeit_msg ctxt "record split_object proof:" split_object_prf;
 
 
     fun split_ex_prf () =
@@ -2341,7 +2341,7 @@
       in
         prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
       end;
-    val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
+    val split_ex = timeit_msg ctxt "record split_ex proof:" split_ex_prf;
 
     fun equality_tac thms =
       let
@@ -2359,7 +2359,7 @@
               Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
              (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
           end);
-    val equality = timeit_msg "record equality proof:" equality_prf;
+    val equality = timeit_msg ctxt "record equality proof:" equality_prf;
 
     val ((([sel_convs', upd_convs', sel_defs', upd_defs',
             fold_congs', unfold_congs',
@@ -2411,7 +2411,7 @@
       |> add_extsplit extension_name ext_split
       |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
       |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
-      |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
+      |> add_fieldext (extension_name, snd extension) names
       |> add_code ext_tyco vs extT ext simps' ext_inject
       |> Sign.restore_naming thy;
 
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/General/markup.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -378,12 +378,13 @@
 
 local
   val default = {output = default_output};
-  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
+  val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
 in
-  fun add_mode name output = CRITICAL (fn () =>
-    Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
+  fun add_mode name output =
+    Synchronized.change modes (Symtab.update_new (name, {output = output}));
   fun get_mode () =
-    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
+    the_default default
+      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/General/output.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -55,12 +55,13 @@
 
 local
   val default = {output = default_output, escape = default_escape};
-  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
+  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
 in
-  fun add_mode name output escape = CRITICAL (fn () =>
-    Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
+  fun add_mode name output escape =
+    Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
   fun get_mode () =
-    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
+    the_default default
+      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
 fun output_width x = #output (get_mode ()) x;
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/General/pretty.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -75,12 +75,13 @@
 
 local
   val default = {indent = default_indent};
-  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
+  val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
 in
-  fun add_mode name indent = CRITICAL (fn () =>
-    Unsynchronized.change modes (Symtab.update_new (name, {indent = indent})));
+  fun add_mode name indent =
+    Synchronized.change modes (Symtab.update_new (name, {indent = indent}));
   fun get_mode () =
-    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
+    the_default default
+      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
 fun mode_indent x y = #indent (get_mode ()) x y;
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/Isar/code.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -247,11 +247,12 @@
 
 type kind = { empty: Object.T };
 
-val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
+val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table);
 
-fun invoke f k = case Datatab.lookup (! kinds) k
- of SOME kind => f kind
-  | NONE => raise Fail "Invalid code data identifier";
+fun invoke f k =
+  (case Datatab.lookup (Synchronized.value kinds) k of
+    SOME kind => f kind
+  | NONE => raise Fail "Invalid code data identifier");
 
 in
 
@@ -259,7 +260,7 @@
   let
     val k = serial ();
     val kind = { empty = empty };
-    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
+    val _ = Synchronized.change kinds (Datatab.update (k, kind));
   in k end;
 
 fun invoke_init k = invoke (fn kind => #empty kind) k;
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/ROOT.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -20,6 +20,13 @@
 use "General/print_mode.ML";
 use "General/alist.ML";
 use "General/table.ML";
+
+use "Concurrent/simple_thread.ML";
+
+use "Concurrent/synchronized.ML";
+if Multithreading.available then ()
+else use "Concurrent/synchronized_sequential.ML";
+
 use "General/output.ML";
 use "General/timing.ML";
 use "General/properties.ML";
@@ -63,16 +70,10 @@
 
 (* concurrency within the ML runtime *)
 
-use "Concurrent/simple_thread.ML";
-
 use "Concurrent/single_assignment.ML";
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";
 
-use "Concurrent/synchronized.ML";
-if Multithreading.available then ()
-else use "Concurrent/synchronized_sequential.ML";
-
 if String.isPrefix "smlnj" ml_system then ()
 else use "Concurrent/time_limit.ML";
 
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -20,7 +20,7 @@
   val is_active: unit -> bool
   val add_command: string -> (string list -> unit) -> unit
   val command: string -> string list -> unit
-  val crashes: exn list Unsynchronized.ref
+  val crashes: exn list Synchronized.var
   val init: string -> string -> unit
 end;
 
@@ -41,18 +41,19 @@
 
 local
 
-val global_commands = Unsynchronized.ref (Symtab.empty: (string list -> unit) Symtab.table);
+val commands =
+  Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table);
 
 in
 
-fun add_command name cmd = CRITICAL (fn () =>
-  Unsynchronized.change global_commands (fn cmds =>
+fun add_command name cmd =
+  Synchronized.change commands (fn cmds =>
    (if not (Symtab.defined cmds name) then ()
     else warning ("Redefining Isabelle process command " ^ quote name);
-    Symtab.update (name, cmd) cmds)));
+    Symtab.update (name, cmd) cmds));
 
 fun command name args =
-  (case Symtab.lookup (! global_commands) name of
+  (case Symtab.lookup (Synchronized.value commands) name of
     NONE => error ("Undefined Isabelle process command " ^ quote name)
   | SOME cmd => cmd args);
 
@@ -118,12 +119,12 @@
 
 (* protocol loop -- uninterruptible *)
 
-val crashes = Unsynchronized.ref ([]: exn list);
+val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
 
 local
 
 fun recover crash =
-  (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
+  (Synchronized.change crashes (cons crash);
     warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
 
 fun read_chunk stream len =
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/System/isar.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -17,7 +17,7 @@
   val undo: int -> unit
   val kill: unit -> unit
   val kill_proof: unit -> unit
-  val crashes: exn list Unsynchronized.ref
+  val crashes: exn list Synchronized.var
   val toplevel_loop: TextIO.instream ->
     {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   val loop: unit -> unit
@@ -113,7 +113,7 @@
 
 (* toplevel loop -- uninterruptible *)
 
-val crashes = Unsynchronized.ref ([]: exn list);
+val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
 
 local
 
@@ -128,7 +128,7 @@
     handle exn =>
       (Output.error_msg (ML_Compiler.exn_message exn)
         handle crash =>
-          (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
+          (Synchronized.change crashes (cons crash);
             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
         raw_loop secure src)
   end;
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/context.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -128,10 +128,10 @@
   extend: Object.T -> Object.T,
   merge: pretty -> Object.T * Object.T -> Object.T};
 
-val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
+val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
 
 fun invoke name f k x =
-  (case Datatab.lookup (! kinds) k of
+  (case Datatab.lookup (Synchronized.value kinds) k of
     SOME kind =>
       if ! timing andalso name <> "" then
         Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind))
@@ -149,7 +149,7 @@
   let
     val k = serial ();
     val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
-    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
+    val _ = Synchronized.change kinds (Datatab.update (k, kind));
   in k end;
 
 val extend_data = Datatab.map invoke_extend;
@@ -475,15 +475,15 @@
 
 local
 
-val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
+val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Object.T) Datatab.table);
 
 fun invoke_init k =
-  (case Datatab.lookup (! kinds) k of
+  (case Datatab.lookup (Synchronized.value kinds) k of
     SOME init => init
   | NONE => raise Fail "Invalid proof data identifier");
 
 fun init_data thy =
-  Datatab.map (fn k => fn _ => invoke_init k thy) (! kinds);
+  Datatab.map (fn k => fn _ => invoke_init k thy) (Synchronized.value kinds);
 
 fun init_new_data data thy =
   Datatab.merge (K true) (data, init_data thy);
@@ -511,7 +511,7 @@
 fun declare init =
   let
     val k = serial ();
-    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
+    val _ = Synchronized.change kinds (Datatab.update (k, init));
   in k end;
 
 fun get k dest prf =
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/name.ML
--- a/src/Pure/name.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/name.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -7,6 +7,7 @@
 signature NAME =
 sig
   val uu: string
+  val uu_: string
   val aT: string
   val bound: int -> string
   val is_bound: string -> bool
@@ -35,6 +36,7 @@
 (** common defaults **)
 
 val uu = "uu";
+val uu_ = "uu_";
 val aT = "'a";
 
 
diff -r b46f5d2d42cc -r 93dcfcf91484 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Jul 06 17:19:34 2011 +0100
+++ b/src/Pure/term.ML	Wed Jul 06 23:11:59 2011 +0200
@@ -762,7 +762,7 @@
 
 (*Form an abstraction over a free variable.*)
 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
-fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body);
+fun absdummy (T, body) = Abs (Name.uu_, T, body);
 
 (*Abstraction over a list of free variables*)
 fun list_abs_free ([ ] ,     t) = t