prefer Synchronized.var;

--- a/src/Pure/General/markup.ML	Wed Jul 06 20:14:13 2011 +0200
+++ b/src/Pure/General/markup.ML	Wed Jul 06 20:46:06 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;

--- a/src/Pure/General/output.ML	Wed Jul 06 20:14:13 2011 +0200
+++ b/src/Pure/General/output.ML	Wed Jul 06 20:46:06 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;

--- a/src/Pure/General/pretty.ML	Wed Jul 06 20:14:13 2011 +0200
+++ b/src/Pure/General/pretty.ML	Wed Jul 06 20:46:06 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;

--- a/src/Pure/Isar/code.ML	Wed Jul 06 20:14:13 2011 +0200
+++ b/src/Pure/Isar/code.ML	Wed Jul 06 20:46:06 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;

--- a/src/Pure/ROOT.ML	Wed Jul 06 20:14:13 2011 +0200
+++ b/src/Pure/ROOT.ML	Wed Jul 06 20:46:06 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";
 

--- a/src/Pure/System/isabelle_process.ML	Wed Jul 06 20:14:13 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Jul 06 20:46:06 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 =

--- a/src/Pure/System/isar.ML	Wed Jul 06 20:14:13 2011 +0200
+++ b/src/Pure/System/isar.ML	Wed Jul 06 20:46:06 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;

--- a/src/Pure/context.ML	Wed Jul 06 20:14:13 2011 +0200
+++ b/src/Pure/context.ML	Wed Jul 06 20:46:06 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 =