# HG changeset patch
# User wenzelm
# Date 1254217762 -7200
# Node ID 15bb09ca0378b6f9bd23f69f8c8a7835786655fc
# Parent  76fa673eee8b09645e7ba24a584d8e62ea53039a
explicit indication of Unsynchronized.ref;

diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -99,13 +99,13 @@
 
 (* global state *)
 
-val queue = ref Task_Queue.empty;
-val next = ref 0;
-val workers = ref ([]: (Thread.thread * bool) list);
-val scheduler = ref (NONE: Thread.thread option);
-val excessive = ref 0;
-val canceled = ref ([]: Task_Queue.group list);
-val do_shutdown = ref false;
+val queue = Unsynchronized.ref Task_Queue.empty;
+val next = Unsynchronized.ref 0;
+val workers = Unsynchronized.ref ([]: (Thread.thread * bool) list);
+val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
+val excessive = Unsynchronized.ref 0;
+val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
+val do_shutdown = Unsynchronized.ref false;
 
 
 (* synchronization *)
@@ -162,7 +162,8 @@
   in (result, job) end;
 
 fun do_cancel group = (*requires SYNCHRONIZED*)
- (change canceled (insert Task_Queue.eq_group group); broadcast scheduler_event);
+ (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
+  broadcast scheduler_event);
 
 fun execute name (task, group, jobs) =
   let
@@ -171,7 +172,7 @@
       fold (fn job => fn ok => job valid andalso ok) jobs true) ();
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
-        val maximal = change_result queue (Task_Queue.finish task);
+        val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
         val _ =
           if ok then ()
           else if Task_Queue.cancel (! queue) group then ()
@@ -188,7 +189,8 @@
   fold (fn (_, active) => fn i => if active then i + 1 else i) (! workers) 0;
 
 fun change_active active = (*requires SYNCHRONIZED*)
-  change workers (AList.update Thread.equal (Thread.self (), active));
+  Unsynchronized.change workers
+    (AList.update Thread.equal (Thread.self (), active));
 
 
 (* worker threads *)
@@ -198,14 +200,15 @@
 
 fun worker_next () = (*requires SYNCHRONIZED*)
   if ! excessive > 0 then
-    (dec excessive;
-     change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
+    (Unsynchronized.dec excessive;
+     Unsynchronized.change workers
+      (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
      broadcast scheduler_event;
      NONE)
   else if count_active () > Multithreading.max_threads_value () then
     (worker_wait scheduler_event; worker_next ())
   else
-    (case change_result queue (Task_Queue.dequeue (Thread.self ())) of
+    (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of
       NONE => (worker_wait work_available; worker_next ())
     | some => some);
 
@@ -215,13 +218,13 @@
   | SOME work => (execute name work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
-  change workers (cons (SimpleThread.fork false (fn () =>
+  Unsynchronized.change workers (cons (SimpleThread.fork false (fn () =>
      (broadcast scheduler_event; worker_loop name)), true));
 
 
 (* scheduler *)
 
-val last_status = ref Time.zeroTime;
+val last_status = Unsynchronized.ref Time.zeroTime;
 val next_status = Time.fromMilliseconds 500;
 val next_round = Time.fromMilliseconds 50;
 
@@ -263,7 +266,8 @@
     val _ = excessive := l - mm;
     val _ =
       if mm > l then
-        funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
+        funpow (mm - l) (fn () =>
+          worker_start ("worker " ^ string_of_int (Unsynchronized.inc next))) ()
       else ();
 
     (*canceled groups*)
@@ -272,7 +276,7 @@
       else
        (Multithreading.tracing 1 (fn () =>
           string_of_int (length (! canceled)) ^ " canceled groups");
-        change canceled (filter_out (Task_Queue.cancel (! queue)));
+        Unsynchronized.change canceled (filter_out (Task_Queue.cancel (! queue)));
         broadcast_work ());
 
     (*delay loop*)
@@ -317,7 +321,8 @@
     val (result, job) = future_job group e;
     val task = SYNCHRONIZED "enqueue" (fn () =>
       let
-        val (task, minimal) = change_result queue (Task_Queue.enqueue group deps pri job);
+        val (task, minimal) =
+          Unsynchronized.change_result queue (Task_Queue.enqueue group deps pri job);
         val _ = if minimal then signal work_available else ();
         val _ = scheduler_check ();
       in task end);
@@ -347,7 +352,7 @@
 fun join_next deps = (*requires SYNCHRONIZED*)
   if null deps then NONE
   else
-    (case change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
+    (case Unsynchronized.change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
       (NONE, []) => NONE
     | (NONE, deps') => (worker_wait work_finished; join_next deps')
     | (SOME work, deps') => SOME (work, deps'));
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -24,13 +24,13 @@
  {name: string,
   lock: Mutex.mutex,
   cond: ConditionVar.conditionVar,
-  var: 'a ref};
+  var: 'a Unsynchronized.ref};
 
 fun var name x = Var
  {name = name,
   lock = Mutex.mutex (),
   cond = ConditionVar.conditionVar (),
-  var = ref x};
+  var = Unsynchronized.ref x};
 
 fun value (Var {var, ...}) = ! var;
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Concurrent/synchronized_dummy.ML
--- a/src/Pure/Concurrent/synchronized_dummy.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Concurrent/synchronized_dummy.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -7,9 +7,9 @@
 structure Synchronized: SYNCHRONIZED =
 struct
 
-datatype 'a var = Var of 'a ref;
+datatype 'a var = Var of 'a Unsynchronized.ref;
 
-fun var _ x = Var (ref x);
+fun var _ x = Var (Unsynchronized.ref x);
 fun value (Var var) = ! var;
 
 fun timed_access (Var var) _ f =
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/file.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -85,7 +85,8 @@
 (* file identification *)
 
 local
-  val ident_cache = ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
+  val ident_cache =
+    Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
 in
 
 fun check_cache (path, time) = CRITICAL (fn () =>
@@ -94,7 +95,8 @@
   | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
 
 fun update_cache (path, (time, id)) = CRITICAL (fn () =>
-  change ident_cache (Symtab.update (path, {time_stamp = time, id = id})));
+  Unsynchronized.change ident_cache
+    (Symtab.update (path, {time_stamp = time, id = id})));
 
 end;
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/General/lazy.ML
--- a/src/Pure/General/lazy.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/lazy.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -26,12 +26,12 @@
   Lazy of unit -> 'a |
   Result of 'a Exn.result;
 
-type 'a lazy = 'a T ref;
+type 'a lazy = 'a T Unsynchronized.ref;
 
 fun same (r1: 'a lazy, r2) = r1 = r2;
 
-fun lazy e = ref (Lazy e);
-fun value x = ref (Result (Exn.Result x));
+fun lazy e = Unsynchronized.ref (Lazy e);
+fun value x = Unsynchronized.ref (Result (Exn.Result x));
 
 fun peek r =
   (case ! r of
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/markup.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -323,10 +323,10 @@
 
 local
   val default = {output = default_output};
-  val modes = ref (Symtab.make [("", default)]);
+  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
 in
   fun add_mode name output = CRITICAL (fn () =>
-    change modes (Symtab.update_new (name, {output = output})));
+    Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
   fun get_mode () =
     the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/name_space.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -9,9 +9,9 @@
 
 signature BASIC_NAME_SPACE =
 sig
-  val long_names: bool ref
-  val short_names: bool ref
-  val unique_names: bool ref
+  val long_names: bool Unsynchronized.ref
+  val short_names: bool Unsynchronized.ref
+  val unique_names: bool Unsynchronized.ref
 end;
 
 signature NAME_SPACE =
@@ -105,9 +105,9 @@
     else ext (get_accesses space name)
   end;
 
-val long_names = ref false;
-val short_names = ref false;
-val unique_names = ref true;
+val long_names = Unsynchronized.ref false;
+val short_names = Unsynchronized.ref false;
+val unique_names = Unsynchronized.ref true;
 
 fun extern space name =
   extern_flags
@@ -261,6 +261,6 @@
 
 end;
 
-structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
-open BasicNameSpace;
+structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
+open Basic_Name_Space;
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/output.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -11,13 +11,13 @@
   val priority: string -> unit
   val tracing: string -> unit
   val warning: string -> unit
-  val tolerate_legacy_features: bool ref
+  val tolerate_legacy_features: bool Unsynchronized.ref
   val legacy_feature: string -> unit
   val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
   val timeit: (unit -> 'a) -> 'a
   val timeap: ('a -> 'b) -> 'a -> 'b
   val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
-  val timing: bool ref
+  val timing: bool Unsynchronized.ref
 end;
 
 signature OUTPUT =
@@ -32,18 +32,18 @@
   val std_output: output -> unit
   val std_error: output -> unit
   val writeln_default: output -> unit
-  val writeln_fn: (output -> unit) ref
-  val priority_fn: (output -> unit) ref
-  val tracing_fn: (output -> unit) ref
-  val warning_fn: (output -> unit) ref
-  val error_fn: (output -> unit) ref
-  val debug_fn: (output -> unit) ref
-  val prompt_fn: (output -> unit) ref
-  val status_fn: (output -> unit) ref
+  val writeln_fn: (output -> unit) Unsynchronized.ref
+  val priority_fn: (output -> unit) Unsynchronized.ref
+  val tracing_fn: (output -> unit) Unsynchronized.ref
+  val warning_fn: (output -> unit) Unsynchronized.ref
+  val error_fn: (output -> unit) Unsynchronized.ref
+  val debug_fn: (output -> unit) Unsynchronized.ref
+  val prompt_fn: (output -> unit) Unsynchronized.ref
+  val status_fn: (output -> unit) Unsynchronized.ref
   val error_msg: string -> unit
   val prompt: string -> unit
   val status: string -> unit
-  val debugging: bool ref
+  val debugging: bool Unsynchronized.ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
 end;
@@ -60,10 +60,10 @@
 
 local
   val default = {output = default_output, escape = default_escape};
-  val modes = ref (Symtab.make [("", default)]);
+  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
 in
   fun add_mode name output escape = CRITICAL (fn () =>
-    change modes (Symtab.update_new (name, {output = output, escape = escape})));
+    Unsynchronized.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 ()));
 end;
@@ -91,14 +91,14 @@
 
 (* Isabelle output channels *)
 
-val writeln_fn = ref writeln_default;
-val priority_fn = ref (fn s => ! writeln_fn s);
-val tracing_fn = ref (fn s => ! writeln_fn s);
-val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
-val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
-val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
-val prompt_fn = ref std_output;
-val status_fn = ref (fn _: string => ());
+val writeln_fn = Unsynchronized.ref writeln_default;
+val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
+val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
+val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
+val prompt_fn = Unsynchronized.ref std_output;
+val status_fn = Unsynchronized.ref (fn _: string => ());
 
 fun writeln s = ! writeln_fn (output s);
 fun priority s = ! priority_fn (output s);
@@ -108,13 +108,13 @@
 fun prompt s = ! prompt_fn (output s);
 fun status s = ! status_fn (output s);
 
-val tolerate_legacy_features = ref true;
+val tolerate_legacy_features = Unsynchronized.ref true;
 fun legacy_feature s =
   (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
 
 fun no_warnings f = setmp warning_fn (K ()) f;
 
-val debugging = ref false;
+val debugging = Unsynchronized.ref false;
 fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
 
 
@@ -140,9 +140,9 @@
 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
 
 (*global timing mode*)
-val timing = ref false;
+val timing = Unsynchronized.ref false;
 
 end;
 
-structure BasicOutput: BASIC_OUTPUT = Output;
-open BasicOutput;
+structure Basic_Output: BASIC_OUTPUT = Output;
+open Basic_Output;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/pretty.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -86,10 +86,10 @@
 
 local
   val default = {indent = default_indent};
-  val modes = ref (Symtab.make [("", default)]);
+  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
 in
   fun add_mode name indent = CRITICAL (fn () =>
-    change modes (Symtab.update_new (name, {indent = indent})));
+    Unsynchronized.change modes (Symtab.update_new (name, {indent = indent})));
   fun get_mode () =
     the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
@@ -186,14 +186,14 @@
   breakgain = m div 20,         (*minimum added space required of a break*)
   emergencypos = m div 2};      (*position too far to right*)
 
-val margin_info = ref (make_margin_info 76);
+val margin_info = Unsynchronized.ref (make_margin_info 76);
 fun setmargin m = margin_info := make_margin_info m;
 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
 
 
 (* depth limitation *)
 
-val depth = ref 0;   (*maximum depth; 0 means no limit*)
+val depth = Unsynchronized.ref 0;   (*maximum depth; 0 means no limit*)
 fun setdepth dp = (depth := dp);
 
 local
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/print_mode.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -7,9 +7,9 @@
 
 signature BASIC_PRINT_MODE =
 sig
-  val print_mode: string list ref            (*global template*)
-  val print_mode_value: unit -> string list  (*thread-local value*)
-  val print_mode_active: string -> bool      (*thread-local value*)
+  val print_mode: string list Unsynchronized.ref  (*global template*)
+  val print_mode_value: unit -> string list       (*thread-local value*)
+  val print_mode_active: string -> bool           (*thread-local value*)
 end;
 
 signature PRINT_MODE =
@@ -28,7 +28,7 @@
 val input = "input";
 val internal = "internal";
 
-val print_mode = ref ([]: string list);
+val print_mode = Unsynchronized.ref ([]: string list);
 val tag = Universal.tag () : string list option Universal.tag;
 
 fun print_mode_value () =
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/secure.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -23,7 +23,7 @@
 
 (** secure flag **)
 
-val secure = ref false;
+val secure = Unsynchronized.ref false;
 
 fun set_secure () = secure := true;
 fun is_secure () = ! secure;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/code.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -217,8 +217,8 @@
   purge: theory -> string list -> Object.T -> Object.T
 };
 
-val kinds = ref (Datatab.empty: kind Datatab.table);
-val kind_keys = ref ([]: serial list);
+val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
+val kind_keys = Unsynchronized.ref ([]: serial list);
 
 fun invoke f k = case Datatab.lookup (! kinds) k
  of SOME kind => f kind
@@ -230,8 +230,8 @@
   let
     val k = serial ();
     val kind = {empty = empty, purge = purge};
-    val _ = change kinds (Datatab.update (k, kind));
-    val _ = change kind_keys (cons k);
+    val _ = Unsynchronized.change kinds (Datatab.update (k, kind));
+    val _ = Unsynchronized.change kind_keys (cons k);
   in k end;
 
 fun invoke_init k = invoke (fn kind => #empty kind) k;
@@ -252,13 +252,13 @@
 
 structure Code_Data = TheoryDataFun
 (
-  type T = spec * data ref;
+  type T = spec * data Unsynchronized.ref;
   val empty = (make_spec (false,
-    (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), ref empty_data);
-  fun copy (spec, data) = (spec, ref (! data));
+    (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
+  fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
   val extend = copy;
   fun merge pp ((spec1, data1), (spec2, data2)) =
-    (merge_spec (spec1, spec2), ref empty_data);
+    (merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
 );
 
 fun thy_data f thy = f ((snd o Code_Data.get) thy);
@@ -267,7 +267,7 @@
   case Datatab.lookup (! data_ref) kind
    of SOME x => x
     | NONE => let val y = invoke_init kind
-        in (change data_ref (Datatab.update (kind, y)); y) end;
+        in (Unsynchronized.change data_ref (Datatab.update (kind, y)); y) end;
 
 in
 
@@ -281,11 +281,11 @@
     | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
 
 fun map_exec_purge touched f thy =
-  Code_Data.map (fn (exec, data) => (f exec, ref (case touched
+  Code_Data.map (fn (exec, data) => (f exec, Unsynchronized.ref (case touched
    of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
     | NONE => empty_data))) thy;
 
-val purge_data = (Code_Data.map o apsnd) (K (ref empty_data));
+val purge_data = (Code_Data.map o apsnd) (K (Unsynchronized.ref empty_data));
 
 fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
   o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
@@ -332,7 +332,7 @@
       let
         val data = get_ensure_init kind data_ref;
         val data' = f (dest data);
-      in (change data_ref (Datatab.update (kind, mk data')); data') end;
+      in (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
   in thy_data chnge end;
 
 fun change_yield_data (kind, mk, dest) =
@@ -341,7 +341,7 @@
       let
         val data = get_ensure_init kind data_ref;
         val (x, data') = f (dest data);
-      in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end;
+      in (x, (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
   in thy_data chnge end;
 
 end; (*local*)
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -112,18 +112,18 @@
 (** global configuration **)
 
 local
-  val global_states = ref (Symtab.empty: Toplevel.state option future Symtab.table);
-  val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
-  val global_documents = ref (Symtab.empty: document Symtab.table);
+  val global_states = Unsynchronized.ref (Symtab.empty: Toplevel.state option future Symtab.table);
+  val global_commands = Unsynchronized.ref (Symtab.empty: Toplevel.transition Symtab.table);
+  val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
 in
 
-fun change_states f = NAMED_CRITICAL "Isar" (fn () => change global_states f);
+fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
 fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
 
-fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
+fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
 fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
 
-fun change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
+fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
 fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
 
 fun init () = NAMED_CRITICAL "Isar" (fn () =>
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/local_syntax.ML
--- a/src/Pure/Isar/local_syntax.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/local_syntax.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -4,7 +4,7 @@
 Local syntax depending on theory syntax.
 *)
 
-val show_structs = ref false;
+val show_structs = Unsynchronized.ref false;
 
 signature LOCAL_SYNTAX =
 sig
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/method.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -8,7 +8,7 @@
 sig
   val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
   val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
-  val trace_rules: bool ref
+  val trace_rules: bool Unsynchronized.ref
 end;
 
 signature METHOD =
@@ -215,7 +215,7 @@
 
 (* rule etc. -- single-step refinements *)
 
-val trace_rules = ref false;
+val trace_rules = Unsynchronized.ref false;
 
 fun trace ctxt rules =
   if ! trace_rules andalso not (null rules) then
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -116,16 +116,16 @@
 
 local
 
-val global_commands = ref (Symtab.empty: T Symtab.table);
-val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
+val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
+val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
 
 in
 
 fun get_commands () = CRITICAL (fn () => ! global_commands);
 fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
 
-fun change_commands f = CRITICAL (fn () => change global_commands f);
-fun change_lexicons f = CRITICAL (fn () => change global_lexicons f);
+fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
+fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
 
 end;
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -83,7 +83,7 @@
 datatype slot =
   Slot |
   Value of value option |
-  Assignable of value option ref;
+  Assignable of value option Unsynchronized.ref;
 
 
 (* datatype token *)
@@ -245,7 +245,7 @@
 (* static binding *)
 
 (*1st stage: make empty slots assignable*)
-fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (ref NONE))
+fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
   | assignable tok = tok;
 
 (*2nd stage: assign values as side-effect of scanning*)
@@ -253,7 +253,7 @@
   | assign _ _ = ();
 
 (*3rd stage: static closure of final values*)
-fun closure (Token (x, y, Assignable (ref v))) = Token (x, y, Value v)
+fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
   | closure tok = tok;
 
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -88,11 +88,11 @@
 
 local
 
-val global_commands = ref (Symtab.empty: command Symtab.table);
-val global_markups = ref ([]: (string * ThyOutput.markup) list);
+val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
+val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
 
 fun change_commands f = CRITICAL (fn () =>
- (change global_commands f;
+ (Unsynchronized.change global_commands f;
   global_markups :=
     Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
       (! global_commands) []));
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -30,8 +30,8 @@
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
   val get_goal: state -> context * (thm list * thm)
-  val show_main_goal: bool ref
-  val verbose: bool ref
+  val show_main_goal: bool Unsynchronized.ref
+  val verbose: bool Unsynchronized.ref
   val pretty_state: int -> state -> Pretty.T list
   val pretty_goals: bool -> state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
@@ -315,7 +315,7 @@
 
 (** pretty_state **)
 
-val show_main_goal = ref false;
+val show_main_goal = Unsynchronized.ref false;
 val verbose = ProofContext.verbose;
 
 fun pretty_facts _ _ NONE = []
@@ -930,8 +930,8 @@
 
 fun gen_show prep_att prepp before_qed after_qed stmt int state =
   let
-    val testing = ref false;
-    val rule = ref (NONE: thm option);
+    val testing = Unsynchronized.ref false;
+    val rule = Unsynchronized.ref (NONE: thm option);
     fun fail_msg ctxt =
       "Local statement will fail to refine any pending goal" ::
       (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -123,15 +123,15 @@
   val add_abbrev: string -> Properties.T ->
     binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
-  val verbose: bool ref
+  val verbose: bool Unsynchronized.ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
   val print_binds: Proof.context -> unit
   val print_lthms: Proof.context -> unit
   val print_cases: Proof.context -> unit
-  val debug: bool ref
-  val prems_limit: int ref
+  val debug: bool Unsynchronized.ref
+  val prems_limit: int Unsynchronized.ref
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
   val query_type: Proof.context -> string -> Properties.T
@@ -1208,9 +1208,9 @@
 
 (** print context information **)
 
-val debug = ref false;
+val debug = Unsynchronized.ref false;
 
-val verbose = ref false;
+val verbose = Unsynchronized.ref false;
 fun verb f x = if ! verbose then f (x ()) else [];
 
 fun setmp_verbose f x = Library.setmp verbose true f x;
@@ -1320,7 +1320,7 @@
 
 (* core context *)
 
-val prems_limit = ref ~1;
+val prems_limit = Unsynchronized.ref ~1;
 
 fun pretty_ctxt ctxt =
   if ! prems_limit < 0 andalso not (! debug) then []
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -24,12 +24,12 @@
   val enter_proof_body: state -> Proof.state
   val print_state_context: state -> unit
   val print_state: bool -> state -> unit
-  val quiet: bool ref
-  val debug: bool ref
-  val interact: bool ref
-  val timing: bool ref
-  val profiling: int ref
-  val skip_proofs: bool ref
+  val quiet: bool Unsynchronized.ref
+  val debug: bool Unsynchronized.ref
+  val interact: bool Unsynchronized.ref
+  val timing: bool Unsynchronized.ref
+  val profiling: int Unsynchronized.ref
+  val skip_proofs: bool Unsynchronized.ref
   exception TERMINATE
   exception TOPLEVEL_ERROR
   val program: (unit -> 'a) -> 'a
@@ -216,12 +216,12 @@
 
 (** toplevel transitions **)
 
-val quiet = ref false;
+val quiet = Unsynchronized.ref false;
 val debug = Output.debugging;
-val interact = ref false;
+val interact = Unsynchronized.ref false;
 val timing = Output.timing;
-val profiling = ref 0;
-val skip_proofs = ref false;
+val profiling = Unsynchronized.ref 0;
+val skip_proofs = Unsynchronized.ref false;
 
 exception TERMINATE = Runtime.TERMINATE;
 exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
@@ -550,9 +550,9 @@
 
 (* post-transition hooks *)
 
-local val hooks = ref ([]: (transition -> state -> state -> unit) list) in
+local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
 
-fun add_hook f = CRITICAL (fn () => change hooks (cons f));
+fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
 fun get_hooks () = CRITICAL (fn () => ! hooks);
 
 end;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ML-Systems/compiler_polyml-5.0.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -5,11 +5,11 @@
 
 fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
   let
-    val in_buffer = ref (explode (tune_source txt));
-    val out_buffer = ref ([]: string list);
+    val in_buffer = Unsynchronized.ref (explode (tune_source txt));
+    val out_buffer = Unsynchronized.ref ([]: string list);
     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
 
-    val current_line = ref line;
+    val current_line = Unsynchronized.ref line;
     fun get () =
       (case ! in_buffer of
         [] => ""
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ML-Systems/compiler_polyml-5.2.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -14,9 +14,9 @@
 fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
     (start_line, name) verbose txt =
   let
-    val current_line = ref start_line;
-    val in_buffer = ref (String.explode (tune_source txt));
-    val out_buffer = ref ([]: string list);
+    val current_line = Unsynchronized.ref start_line;
+    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
+    val out_buffer = Unsynchronized.ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
 
     fun get () =
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ML-Systems/compiler_polyml-5.3.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -14,9 +14,9 @@
 fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
     (start_line, name) verbose txt =
   let
-    val line = ref start_line;
-    val in_buffer = ref (String.explode (tune_source txt));
-    val out_buffer = ref ([]: string list);
+    val line = Unsynchronized.ref start_line;
+    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
+    val out_buffer = Unsynchronized.ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
 
     fun get () =
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -31,7 +31,7 @@
 
 val available = true;
 
-val max_threads = ref 0;
+val max_threads = Unsynchronized.ref 0;
 
 val tested_platform =
   let val ml_platform = getenv "ML_PLATFORM"
@@ -114,7 +114,7 @@
 
 (* tracing *)
 
-val trace = ref 0;
+val trace = Unsynchronized.ref 0;
 
 fun tracing level msg =
   if level > ! trace then ()
@@ -148,7 +148,7 @@
 fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
   let
     val worker = Thread.self ();
-    val timeout = ref false;
+    val timeout = Unsynchronized.ref false;
     val watchdog = Thread.fork (fn () =>
       (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
 
@@ -173,7 +173,7 @@
 
     (*result state*)
     datatype result = Wait | Signal | Result of int;
-    val result = ref Wait;
+    val result = Unsynchronized.ref Wait;
     val lock = Mutex.mutex ();
     val cond = ConditionVar.conditionVar ();
     fun set_result res =
@@ -231,8 +231,8 @@
 local
 
 val critical_lock = Mutex.mutex ();
-val critical_thread = ref (NONE: Thread.thread option);
-val critical_name = ref "";
+val critical_thread = Unsynchronized.ref (NONE: Thread.thread option);
+val critical_name = Unsynchronized.ref "";
 
 in
 
@@ -274,7 +274,7 @@
 local
 
 val serial_lock = Mutex.mutex ();
-val serial_count = ref 0;
+val serial_count = Unsynchronized.ref 0;
 
 in
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -91,8 +91,8 @@
       if null toks then Position.none
       else ML_Lex.end_pos_of (List.last toks);
 
-    val input_buffer = ref (input @ [(offset_of end_pos, #"\n")]);
-    val line = ref (the_default 1 (Position.line_of pos));
+    val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
+    val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
 
     fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
     fun get () =
@@ -106,9 +106,9 @@
 
     (* output *)
 
-    val output_buffer = ref Buffer.empty;
+    val output_buffer = Unsynchronized.ref Buffer.empty;
     fun output () = Buffer.content (! output_buffer);
-    fun put s = change output_buffer (Buffer.add s);
+    fun put s = Unsynchronized.change output_buffer (Buffer.add s);
 
     fun put_message {message, hard, location, context = _} =
      (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML/ml_context.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -19,20 +19,21 @@
   val the_global_context: unit -> theory
   val the_local_context: unit -> Proof.context
   val exec: (unit -> unit) -> Context.generic -> Context.generic
-  val stored_thms: thm list ref
+  val stored_thms: thm list Unsynchronized.ref
   val ml_store_thm: string * thm -> unit
   val ml_store_thms: string * thm list -> unit
   type antiq =
     {struct_name: string, background: Proof.context} ->
       (Proof.context -> string * string) * Proof.context
   val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
-  val trace: bool ref
+  val trace: bool Unsynchronized.ref
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: bool -> Position.T -> Symbol_Pos.text -> unit
   val eval_file: Path.T -> unit
   val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
-  val evaluate: Proof.context -> bool -> string * (unit -> 'a) option ref -> string -> 'a
+  val evaluate: Proof.context -> bool ->
+    string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
   val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
 end
 
@@ -53,7 +54,7 @@
 
 (* theorem bindings *)
 
-val stored_thms: thm list ref = ref [];
+val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref [];
 
 fun ml_store sel (name, ths) =
   let
@@ -89,12 +90,13 @@
 
 local
 
-val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
+val global_parsers =
+  Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
 
 in
 
 fun add_antiq name scan = CRITICAL (fn () =>
-  change global_parsers (fn tab =>
+  Unsynchronized.change global_parsers (fn tab =>
    (if not (Symtab.defined tab name) then ()
     else warning ("Redefined ML antiquotation: " ^ quote name);
     Symtab.update (name, scan) tab)));
@@ -162,7 +164,7 @@
         in (ml, SOME (Context.Proof ctxt')) end;
   in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
 
-val trace = ref false;
+val trace = Unsynchronized.ref false;
 
 fun eval verbose pos txt =
   let
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -91,7 +91,7 @@
       Pattern.rewrite_term thy [] (condrew' :: procs) tm
     and condrew' tm =
       let
-        val cache = ref ([] : (term * term) list);
+        val cache = Unsynchronized.ref ([] : (term * term) list);
         fun lookup f x = (case AList.lookup (op =) (!cache) x of
             NONE =>
               let val y = f x
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -6,7 +6,7 @@
 
 signature RECONSTRUCT =
 sig
-  val quiet_mode : bool ref
+  val quiet_mode : bool Unsynchronized.ref
   val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
   val prop_of' : term list -> Proofterm.proof -> term
   val prop_of : Proofterm.proof -> term
@@ -19,7 +19,7 @@
 
 open Proofterm;
 
-val quiet_mode = ref true;
+val quiet_mode = Unsynchronized.ref true;
 fun message s = if !quiet_mode then () else writeln s;
 
 fun vars_of t = map Var (rev (Term.add_vars t []));
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -18,11 +18,11 @@
     get: unit -> string,
     set: string -> unit}
   val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
-    'a ref -> string -> string -> preference
-  val string_pref: string ref -> string -> string -> preference
-  val int_pref: int ref -> string -> string -> preference
-  val nat_pref: int ref -> string -> string -> preference
-  val bool_pref: bool ref -> string -> string -> preference
+    'a Unsynchronized.ref -> string -> string -> preference
+  val string_pref: string Unsynchronized.ref -> string -> string -> preference
+  val int_pref: int Unsynchronized.ref -> string -> string -> preference
+  val nat_pref: int Unsynchronized.ref -> string -> string -> preference
+  val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
   type T = (string * preference list) list
   val pure_preferences: T
   val remove: string -> T -> T
@@ -95,8 +95,9 @@
   let
     fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
     fun set s =
-      if PgipTypes.read_pgipbool s then change print_mode (insert (op =) thm_depsN)
-      else change print_mode (remove (op =) thm_depsN);
+      if PgipTypes.read_pgipbool s
+      then Unsynchronized.change print_mode (insert (op =) thm_depsN)
+      else Unsynchronized.change print_mode (remove (op =) thm_depsN);
   in
     mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
       "Track theorem dependencies within Proof General"
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -226,7 +226,7 @@
 
 (* init *)
 
-val initialized = ref false;
+val initialized = Unsynchronized.ref false;
 
 fun init false = panic "No Proof General interface support for Isabelle/classic mode."
   | init true =
@@ -239,9 +239,9 @@
           ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
           setup_thy_loader ();
           setup_present_hook ();
-          set initialized);
+          Unsynchronized.set initialized);
         sync_thy_loader ();
-       change print_mode (update (op =) proof_generalN);
+       Unsynchronized.change print_mode (update (op =) proof_generalN);
        Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
 end;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -32,20 +32,20 @@
 (** print mode **)
 
 val proof_generalN = "ProofGeneral";
-val pgmlsymbols_flag = ref true;
+val pgmlsymbols_flag = Unsynchronized.ref true;
 
 
 (* assembling and issuing PGIP packets *)
 
-val pgip_refid = ref NONE: string option ref;
-val pgip_refseq = ref NONE: int option ref;
+val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
+val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
 
 local
   val pgip_class  = "pg"
   val pgip_tag = "Isabelle/Isar"
-  val pgip_id = ref ""
-  val pgip_seq = ref 0
-  fun pgip_serial () = inc pgip_seq
+  val pgip_id = Unsynchronized.ref ""
+  val pgip_seq = Unsynchronized.ref 0
+  fun pgip_serial () = Unsynchronized.inc pgip_seq
 
   fun assemble_pgips pgips =
     Pgip { tag = SOME pgip_tag,
@@ -65,7 +65,7 @@
 
 fun matching_pgip_id id = (id = ! pgip_id)
 
-val output_xml_fn = ref Output.writeln_default
+val output_xml_fn = Unsynchronized.ref Output.writeln_default
 fun output_xml s = ! output_xml_fn (XML.string_of s);
 
 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
@@ -280,7 +280,7 @@
 
 (* theorem dependeny output *)
 
-val show_theorem_dependencies = ref false;
+val show_theorem_dependencies = Unsynchronized.ref false;
 
 local
 
@@ -368,13 +368,13 @@
 
 (* Preferences: tweak for PGIP interfaces *)
 
-val preferences = ref Preferences.pure_preferences;
+val preferences = Unsynchronized.ref Preferences.pure_preferences;
 
 fun add_preference cat pref =
-  CRITICAL (fn () => change preferences (Preferences.add cat pref));
+  CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
 
 fun setup_preferences_tweak () =
-  CRITICAL (fn () => change preferences
+  CRITICAL (fn () => Unsynchronized.change preferences
    (Preferences.set_default ("show-question-marks", "false") #>
     Preferences.remove "show-question-marks" #>   (* we use markup, not ?s *)
     Preferences.remove "theorem-dependencies" #>  (* set internally *)
@@ -471,7 +471,7 @@
 fun set_proverflag_pgmlsymbols b =
     (pgmlsymbols_flag := b;
       NAMED_CRITICAL "print_mode" (fn () =>
-        change print_mode
+        Unsynchronized.change print_mode
             (fn mode =>
                 remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
 
@@ -677,7 +677,7 @@
    about this special status, but for now we just keep a local reference.
 *)
 
-val currently_open_file = ref (NONE : pgipurl option)
+val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
 
 fun get_currently_open_file () = ! currently_open_file;
 
@@ -779,7 +779,7 @@
 *)
 
 local
-    val current_working_dir = ref (NONE : string option)
+    val current_working_dir = Unsynchronized.ref (NONE : string option)
 in
 fun changecwd_dir newdirpath =
    let
@@ -1021,7 +1021,7 @@
 
 (* init *)
 
-val initialized = ref false;
+val initialized = Unsynchronized.ref false;
 
 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
   | init_pgip true =
@@ -1035,9 +1035,9 @@
          setup_present_hook ();
          init_pgip_session_id ();
          welcome ();
-         set initialized);
+         Unsynchronized.set initialized);
         sync_thy_loader ();
-       change print_mode (update (op =) proof_generalN);
+       Unsynchronized.change print_mode (update (op =) proof_generalN);
        pgip_toplevel tty_src);
 
 
@@ -1045,7 +1045,7 @@
 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
 
 local
-    val pgip_output_channel = ref Output.writeln_default
+    val pgip_output_channel = Unsynchronized.ref Output.writeln_default
 in
 
 (* Set recipient for PGIP results *)
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ROOT.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -8,7 +8,7 @@
 end;
 
 (*if true then some tools will OMIT some proofs*)
-val quick_and_dirty = ref false;
+val quick_and_dirty = Unsynchronized.ref false;
 
 print_depth 10;
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/ast.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -24,8 +24,8 @@
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
   val unfold_ast_p: string -> ast -> ast list * ast
-  val trace_ast: bool ref
-  val stat_ast: bool ref
+  val trace_ast: bool Unsynchronized.ref
+  val stat_ast: bool Unsynchronized.ref
 end;
 
 signature AST =
@@ -173,9 +173,9 @@
 
 fun normalize trace stat get_rules pre_ast =
   let
-    val passes = ref 0;
-    val failed_matches = ref 0;
-    val changes = ref 0;
+    val passes = Unsynchronized.ref 0;
+    val failed_matches = Unsynchronized.ref 0;
+    val changes = Unsynchronized.ref 0;
 
     fun subst _ (ast as Constant _) = ast
       | subst env (Variable x) = the (Symtab.lookup env x)
@@ -184,8 +184,8 @@
     fun try_rules ((lhs, rhs) :: pats) ast =
           (case match ast lhs of
             SOME (env, args) =>
-              (inc changes; SOME (mk_appl (subst env rhs) args))
-          | NONE => (inc failed_matches; try_rules pats ast))
+              (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args))
+          | NONE => (Unsynchronized.inc failed_matches; try_rules pats ast))
       | try_rules [] _ = NONE;
     val try_headless_rules = try_rules (get_rules "");
 
@@ -226,7 +226,7 @@
         val old_changes = ! changes;
         val new_ast = norm ast;
       in
-        inc passes;
+        Unsynchronized.inc passes;
         if old_changes = ! changes then new_ast else normal new_ast
       end;
 
@@ -245,8 +245,8 @@
 
 (* normalize_ast *)
 
-val trace_ast = ref false;
-val stat_ast = ref false;
+val trace_ast = Unsynchronized.ref false;
+val stat_ast = Unsynchronized.ref false;
 
 fun normalize_ast get_rules ast =
   normalize (! trace_ast) (! stat_ast) get_rules ast;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/parser.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -17,7 +17,7 @@
     Tip of Lexicon.token
   val parse: gram -> string -> Lexicon.token list -> parsetree list
   val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
-  val branching_level: int ref
+  val branching_level: int Unsynchronized.ref
 end;
 
 structure Parser: PARSER =
@@ -690,7 +690,7 @@
       else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
 
 
-val branching_level = ref 600;                   (*trigger value for warnings*)
+val branching_level = Unsynchronized.ref 600;   (*trigger value for warnings*)
 
 (*get all productions of a NT and NTs chained to it which can
   be started by specified token*)
@@ -821,7 +821,7 @@
     val Estate = Array.array (s, []);
   in
     Array.update (Estate, 0, S0);
-    get_trees (produce (ref false) prods tags chains Estate 0 indata eof)
+    get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata eof)
   end;
 
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -6,11 +6,11 @@
 
 signature PRINTER0 =
 sig
-  val show_brackets: bool ref
-  val show_sorts: bool ref
-  val show_types: bool ref
-  val show_no_free_types: bool ref
-  val show_all_types: bool ref
+  val show_brackets: bool Unsynchronized.ref
+  val show_sorts: bool Unsynchronized.ref
+  val show_types: bool Unsynchronized.ref
+  val show_no_free_types: bool Unsynchronized.ref
+  val show_all_types: bool Unsynchronized.ref
   val pp_show_brackets: Pretty.pp -> Pretty.pp
 end;
 
@@ -42,11 +42,11 @@
 
 (** options for printing **)
 
-val show_types = ref false;
-val show_sorts = ref false;
-val show_brackets = ref false;
-val show_no_free_types = ref false;
-val show_all_types = ref false;
+val show_types = Unsynchronized.ref false;
+val show_sorts = Unsynchronized.ref false;
+val show_brackets = Unsynchronized.ref false;
+val show_no_free_types = Unsynchronized.ref false;
+val show_all_types = Unsynchronized.ref false;
 
 fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp),
   Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -6,7 +6,7 @@
 
 signature SYN_TRANS0 =
 sig
-  val eta_contract: bool ref
+  val eta_contract: bool Unsynchronized.ref
   val atomic_abs_tr': string * typ * term -> term * term
   val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
   val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
@@ -276,7 +276,7 @@
 
 (*do (partial) eta-contraction before printing*)
 
-val eta_contract = ref true;
+val eta_contract = Unsynchronized.ref true;
 
 fun eta_contr tm =
   let
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -36,9 +36,9 @@
   val print_syntax: syntax -> unit
   val guess_infix: syntax -> string -> mixfix option
   val read_token: string -> Symbol_Pos.T list * Position.T
-  val ambiguity_is_error: bool ref
-  val ambiguity_level: int ref
-  val ambiguity_limit: int ref
+  val ambiguity_is_error: bool Unsynchronized.ref
+  val ambiguity_level: int Unsynchronized.ref
+  val ambiguity_limit: int Unsynchronized.ref
   val standard_parse_term: Pretty.pp -> (term -> string option) ->
     (((string * int) * sort) list -> string * int -> Term.sort) ->
     (string -> bool * string) -> (string -> string option) ->
@@ -472,9 +472,9 @@
 
 (* read_ast *)
 
-val ambiguity_is_error = ref false;
-val ambiguity_level = ref 1;
-val ambiguity_limit = ref 10;
+val ambiguity_is_error = Unsynchronized.ref false;
+val ambiguity_level = Unsynchronized.ref 1;
+val ambiguity_limit = Unsynchronized.ref 10;
 
 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
 
@@ -711,7 +711,7 @@
     unparse_typ: Proof.context -> typ -> Pretty.T,
     unparse_term: Proof.context -> term -> Pretty.T};
 
-  val operations = ref (NONE: operations option);
+  val operations = Unsynchronized.ref (NONE: operations option);
 
   fun operation which ctxt x =
     (case ! operations of
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -130,7 +130,7 @@
 (* init *)
 
 fun init out =
- (change print_mode (update (op =) isabelle_processN);
+ (Unsynchronized.change print_mode (update (op =) isabelle_processN);
   setup_channels out |> init_message;
   OuterKeyword.report ();
   Output.status (Markup.markup Markup.ready "");
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/System/isar.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -18,7 +18,7 @@
   val undo: int -> unit
   val kill: unit -> unit
   val kill_proof: unit -> unit
-  val crashes: exn list ref
+  val crashes: exn list Unsynchronized.ref
   val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   val loop: unit -> unit
   val main: unit -> unit
@@ -36,9 +36,9 @@
   (*previous state, state transition -- regular commands only*)
 
 local
-  val global_history = ref ([]: history);
-  val global_state = ref Toplevel.toplevel;
-  val global_exn = ref (NONE: (exn * string) option);
+  val global_history = Unsynchronized.ref ([]: history);
+  val global_state = Unsynchronized.ref Toplevel.toplevel;
+  val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
 in
 
 fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
@@ -115,7 +115,7 @@
 
 (* toplevel loop *)
 
-val crashes = ref ([]: exn list);
+val crashes = Unsynchronized.ref ([]: exn list);
 
 local
 
@@ -130,7 +130,7 @@
     handle exn =>
       (Output.error_msg (ML_Compiler.exn_message exn)
         handle crash =>
-          (CRITICAL (fn () => change crashes (cons crash));
+          (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
           raw_loop secure src)
   end;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/System/session.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -21,10 +21,10 @@
 
 (* session state *)
 
-val session = ref ([Context.PureN]: string list);
-val session_path = ref ([]: string list);
-val session_finished = ref false;
-val remote_path = ref (NONE: Url.T option);
+val session = Unsynchronized.ref ([Context.PureN]: string list);
+val session_path = Unsynchronized.ref ([]: string list);
+val session_finished = Unsynchronized.ref false;
+val remote_path = Unsynchronized.ref (NONE: Url.T option);
 
 
 (* access path *)
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/html.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -267,8 +267,8 @@
 
 (* document *)
 
-val charset = ref "ISO-8859-1";
-fun with_charset s = setmp_noncritical charset s;
+val charset = Unsynchronized.ref "ISO-8859-1";
+fun with_charset s = setmp_noncritical charset s;   (* FIXME *)
 
 fun begin_document title =
   let val cs = ! charset in
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/present.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -161,10 +161,11 @@
 
 (* state *)
 
-val browser_info = ref empty_browser_info;
-fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
+val browser_info = Unsynchronized.ref empty_browser_info;
+fun change_browser_info f =
+  CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
 
-val suppress_tex_source = ref false;
+val suppress_tex_source = Unsynchronized.ref false;
 fun no_document f x = setmp_noncritical suppress_tex_source true f x;
 
 fun init_theory_info name info =
@@ -229,7 +230,7 @@
 
 (* state *)
 
-val session_info = ref (NONE: session_info option);
+val session_info = Unsynchronized.ref (NONE: session_info option);
 
 fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
 fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
@@ -534,5 +535,5 @@
 
 end;
 
-structure BasicPresent: BASIC_PRESENT = Present;
-open BasicPresent;
+structure Basic_Present: BASIC_PRESENT = Present;
+open Basic_Present;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -50,9 +50,9 @@
 val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
 
 local
-  val hooks = ref ([]: (action -> string -> unit) list);
+  val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
 in
-  fun add_hook f = CRITICAL (fn () => change hooks (cons f));
+  fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
   fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
 end;
 
@@ -111,10 +111,10 @@
 type thy = deps option * theory option;
 
 local
-  val database = ref (Graph.empty: thy Graph.T);
+  val database = Unsynchronized.ref (Graph.empty: thy Graph.T);
 in
   fun get_thys () = ! database;
-  fun change_thys f = CRITICAL (fn () => Library.change database f);
+  fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
 end;
 
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -37,14 +37,16 @@
 
 (* maintain load path *)
 
-local val load_path = ref [Path.current] in
+local val load_path = Unsynchronized.ref [Path.current] in
 
 fun show_path () = map Path.implode (! load_path);
 
-fun del_path s = CRITICAL (fn () => change load_path (remove (op =) (Path.explode s)));
-fun add_path s = CRITICAL (fn () => (del_path s; change load_path (cons (Path.explode s))));
-fun path_add s =
-  CRITICAL (fn () => (del_path s; change load_path (fn path => path @ [Path.explode s])));
+fun del_path s = CRITICAL (fn () =>
+    Unsynchronized.change load_path (remove (op =) (Path.explode s)));
+fun add_path s = CRITICAL (fn () =>
+    (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
+fun path_add s = CRITICAL (fn () =>
+    (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
 fun reset_path () = load_path := [Path.current];
 
 fun with_paths ss f x =
@@ -124,5 +126,5 @@
 
 end;
 
-structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
-open BasicThyLoad;
+structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
+open Basic_Thy_Load;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -6,11 +6,11 @@
 
 signature THY_OUTPUT =
 sig
-  val display: bool ref
-  val quotes: bool ref
-  val indent: int ref
-  val source: bool ref
-  val break: bool ref
+  val display: bool Unsynchronized.ref
+  val quotes: bool Unsynchronized.ref
+  val indent: int Unsynchronized.ref
+  val source: bool Unsynchronized.ref
+  val break: bool Unsynchronized.ref
   val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
   val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
   val defined_command: string -> bool
@@ -21,7 +21,7 @@
   val antiquotation: string -> 'a context_parser ->
     ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
   datatype markup = Markup | MarkupEnv | Verbatim
-  val modes: string list ref
+  val modes: string list Unsynchronized.ref
   val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
@@ -42,11 +42,11 @@
 
 (** global options **)
 
-val display = ref false;
-val quotes = ref false;
-val indent = ref 0;
-val source = ref false;
-val break = ref false;
+val display = Unsynchronized.ref false;
+val quotes = Unsynchronized.ref false;
+val indent = Unsynchronized.ref 0;
+val source = Unsynchronized.ref false;
+val break = Unsynchronized.ref false;
 
 
 
@@ -55,10 +55,10 @@
 local
 
 val global_commands =
-  ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
+  Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
 
 val global_options =
-  ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
+  Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
 
 fun add_item kind (name, x) tab =
  (if not (Symtab.defined tab name) then ()
@@ -67,8 +67,10 @@
 
 in
 
-fun add_commands xs = CRITICAL (fn () => change global_commands (fold (add_item "command") xs));
-fun add_options xs = CRITICAL (fn () => change global_options (fold (add_item "option") xs));
+fun add_commands xs =
+  CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs));
+fun add_options xs =
+  CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs));
 
 fun defined_command name = Symtab.defined (! global_commands) name;
 fun defined_option name = Symtab.defined (! global_options) name;
@@ -143,7 +145,7 @@
 
 (* eval_antiquote *)
 
-val modes = ref ([]: string list);
+val modes = Unsynchronized.ref ([]: string list);
 
 fun eval_antiquote lex state (txt, pos) =
   let
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -9,8 +9,8 @@
   datatype 'term criterion =
     Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
     Pattern of 'term
-  val tac_limit: int ref
-  val limit: int ref
+  val tac_limit: int Unsynchronized.ref
+  val limit: int Unsynchronized.ref
   val find_theorems: Proof.context -> thm option -> int option -> bool ->
     (bool * string criterion) list -> int option * (Facts.ref * thm) list
   val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
@@ -186,7 +186,7 @@
     end
   else NONE
 
-val tac_limit = ref 5;
+val tac_limit = Unsynchronized.ref 5;
 
 fun filter_solves ctxt goal =
   let
@@ -372,7 +372,7 @@
    (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @
     Facts.dest_static [] (ProofContext.facts_of ctxt));
 
-val limit = ref 40;
+val limit = Unsynchronized.ref 40;
 
 fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/codegen.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -6,10 +6,10 @@
 
 signature CODEGEN =
 sig
-  val quiet_mode : bool ref
+  val quiet_mode : bool Unsynchronized.ref
   val message : string -> unit
-  val mode : string list ref
-  val margin : int ref
+  val mode : string list Unsynchronized.ref
+  val margin : int Unsynchronized.ref
   val string_of : Pretty.T -> string
   val str : string -> Pretty.T
 
@@ -75,9 +75,9 @@
   val mk_type: bool -> typ -> Pretty.T
   val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
   val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
-  val test_fn: (int -> term list option) ref
+  val test_fn: (int -> term list option) Unsynchronized.ref
   val test_term: Proof.context -> term -> int -> term list option
-  val eval_result: (unit -> term) ref
+  val eval_result: (unit -> term) Unsynchronized.ref
   val eval_term: theory -> term -> term
   val evaluation_conv: cterm -> thm
   val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
@@ -102,12 +102,12 @@
 structure Codegen : CODEGEN =
 struct
 
-val quiet_mode = ref true;
+val quiet_mode = Unsynchronized.ref true;
 fun message s = if !quiet_mode then () else writeln s;
 
-val mode = ref ([] : string list);
+val mode = Unsynchronized.ref ([] : string list);
 
-val margin = ref 80;
+val margin = Unsynchronized.ref 80;
 
 fun string_of p = (Pretty.string_of |>
   PrintMode.setmp [] |>
@@ -878,7 +878,8 @@
               [mk_gen gr module true xs a T, mk_type true T]) Ts) @
          (if member (op =) xs s then [str a] else []))));
 
-val test_fn : (int -> term list option) ref = ref (fn _ => NONE);
+val test_fn : (int -> term list option) Unsynchronized.ref =
+  Unsynchronized.ref (fn _ => NONE);
 
 fun test_term ctxt t =
   let
@@ -912,7 +913,7 @@
 
 (**** Evaluator for terms ****)
 
-val eval_result = ref (fn () => Bound 0);
+val eval_result = Unsynchronized.ref (fn () => Bound 0);
 
 fun eval_term thy t =
   let
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/context.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -107,7 +107,7 @@
   extend: Object.T -> Object.T,
   merge: Pretty.pp -> Object.T * Object.T -> Object.T};
 
-val kinds = ref (Datatab.empty: kind Datatab.table);
+val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
 
 fun invoke f k =
   (case Datatab.lookup (! kinds) k of
@@ -125,7 +125,7 @@
   let
     val k = serial ();
     val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
-    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
+    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
   in k end;
 
 val copy_data = Datatab.map' invoke_copy;
@@ -149,7 +149,7 @@
 datatype theory =
   Theory of
    (*identity*)
-   {self: theory ref option,      (*dynamic self reference -- follows theory changes*)
+   {self: theory Unsynchronized.ref option,  (*dynamic self reference -- follows theory changes*)
     draft: bool,                  (*draft mode -- linear destructive changes*)
     id: serial,                   (*identifier*)
     ids: unit Inttab.table} *     (*cumulative identifiers of non-drafts -- symbolic body content*)
@@ -186,14 +186,15 @@
 fun eq_id (i: int, j) = i = j;
 
 fun is_stale
-    (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
+    (Theory ({self =
+        SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
       not (eq_id (id, id'))
   | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
 
 fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
   | vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
       let
-        val r = ref thy;
+        val r = Unsynchronized.ref thy;
         val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
       in r := thy'; thy' end;
 
@@ -243,9 +244,9 @@
   theory in external data structures -- a plain theory value would
   become stale as the self reference moves on*)
 
-datatype theory_ref = TheoryRef of theory ref;
+datatype theory_ref = TheoryRef of theory Unsynchronized.ref;
 
-fun deref (TheoryRef (ref thy)) = thy;
+fun deref (TheoryRef (Unsynchronized.ref thy)) = thy;
 
 fun check_thy thy =  (*thread-safe version*)
   let val thy_ref = TheoryRef (the_self thy) in
@@ -437,7 +438,7 @@
 
 local
 
-val kinds = ref (Datatab.empty: (theory -> Object.T) Datatab.table);
+val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
 
 fun invoke_init k =
   (case Datatab.lookup (! kinds) k of
@@ -470,7 +471,7 @@
 fun declare init =
   let
     val k = serial ();
-    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
+    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
   in k end;
 
 fun get k dest prf =
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/display.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -7,10 +7,10 @@
 
 signature BASIC_DISPLAY =
 sig
-  val goals_limit: int ref
-  val show_consts: bool ref
-  val show_hyps: bool ref
-  val show_tags: bool ref
+  val goals_limit: int Unsynchronized.ref
+  val show_consts: bool Unsynchronized.ref
+  val show_hyps: bool Unsynchronized.ref
+  val show_tags: bool Unsynchronized.ref
 end;
 
 signature DISPLAY =
@@ -39,8 +39,8 @@
 val goals_limit = Goal_Display.goals_limit;
 val show_consts = Goal_Display.show_consts;
 
-val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
-val show_tags = ref false;      (*false: suppress tags*)
+val show_hyps = Unsynchronized.ref false;    (*false: print meta-hypotheses as dots*)
+val show_tags = Unsynchronized.ref false;    (*false: suppress tags*)
 
 
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/goal.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -6,7 +6,7 @@
 
 signature BASIC_GOAL =
 sig
-  val parallel_proofs: int ref
+  val parallel_proofs: int Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -102,7 +102,7 @@
 
 (* future_enabled *)
 
-val parallel_proofs = ref 1;
+val parallel_proofs = Unsynchronized.ref 1;
 
 fun future_enabled () =
   Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/goal_display.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -7,8 +7,8 @@
 
 signature GOAL_DISPLAY =
 sig
-  val goals_limit: int ref
-  val show_consts: bool ref
+  val goals_limit: int Unsynchronized.ref
+  val show_consts: bool Unsynchronized.ref
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
     thm -> Pretty.T list
@@ -18,8 +18,8 @@
 structure Goal_Display: GOAL_DISPLAY =
 struct
 
-val goals_limit = ref 10;      (*max number of goals to print*)
-val show_consts = ref false;   (*true: show consts with types in proof state output*)
+val goals_limit = Unsynchronized.ref 10;     (*max number of goals to print*)
+val show_consts = Unsynchronized.ref false;  (*true: show consts with types in proof state output*)
 
 fun pretty_flexpair ctxt (t, u) = Pretty.block
   [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/meta_simplifier.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -11,9 +11,9 @@
 
 signature BASIC_META_SIMPLIFIER =
 sig
-  val debug_simp: bool ref
-  val trace_simp: bool ref
-  val trace_simp_depth_limit: int ref
+  val debug_simp: bool Unsynchronized.ref
+  val trace_simp: bool Unsynchronized.ref
+  val trace_simp_depth_limit: int Unsynchronized.ref
   type rrule
   val eq_rrule: rrule * rrule -> bool
   type simpset
@@ -84,7 +84,7 @@
    {rules: rrule Net.net,
     prems: thm list,
     bounds: int * ((string * typ) * string) list,
-    depth: int * bool ref,
+    depth: int * bool Unsynchronized.ref,
     context: Proof.context option} *
    {congs: (string * thm) list * string list,
     procs: proc Net.net,
@@ -112,7 +112,7 @@
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
   val theory_context: theory  -> simpset -> simpset
-  val debug_bounds: bool ref
+  val debug_bounds: bool Unsynchronized.ref
   val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
   val set_solvers: solver list -> simpset -> simpset
   val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
@@ -190,7 +190,7 @@
    {rules: rrule Net.net,
     prems: thm list,
     bounds: int * ((string * typ) * string) list,
-    depth: int * bool ref,
+    depth: int * bool Unsynchronized.ref,
     context: Proof.context option} *
    {congs: (string * thm) list * string list,
     procs: proc Net.net,
@@ -256,7 +256,7 @@
 val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
 val simp_depth_limit = Config.int simp_depth_limit_value;
 
-val trace_simp_depth_limit = ref 1;
+val trace_simp_depth_limit = Unsynchronized.ref 1;
 
 fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
   if depth > ! trace_simp_depth_limit then
@@ -266,7 +266,8 @@
 
 val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
   (rules, prems, bounds,
-    (depth + 1, if depth = ! trace_simp_depth_limit then ref false else exceeded), context));
+    (depth + 1,
+      if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
 
 fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
 
@@ -275,8 +276,8 @@
 
 exception SIMPLIFIER of string * thm;
 
-val debug_simp = ref false;
-val trace_simp = ref false;
+val debug_simp = Unsynchronized.ref false;
+val trace_simp = Unsynchronized.ref false;
 
 local
 
@@ -746,7 +747,7 @@
 (* empty *)
 
 fun init_ss mk_rews termless subgoal_tac solvers =
-  make_simpset ((Net.empty, [], (0, []), (0, ref false), NONE),
+  make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
     (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
 
 fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
@@ -1209,7 +1210,7 @@
     prover: how to solve premises in conditional rewrites and congruences
 *)
 
-val debug_bounds = ref false;
+val debug_bounds = Unsynchronized.ref false;
 
 fun check_bounds ss ct =
   if ! debug_bounds then
@@ -1337,5 +1338,5 @@
 
 end;
 
-structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
-open BasicMetaSimplifier;
+structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
+open Basic_Meta_Simplifier;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/old_goals.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -19,7 +19,7 @@
   type proof
   val premises: unit -> thm list
   val reset_goals: unit -> unit
-  val result_error_fn: (thm -> string -> thm) ref
+  val result_error_fn: (thm -> string -> thm) Unsynchronized.ref
   val print_sign_exn: theory -> exn -> 'a
   val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
   val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
@@ -233,21 +233,21 @@
 (*** References ***)
 
 (*Current assumption list -- set by "goal".*)
-val curr_prems = ref([] : thm list);
+val curr_prems = Unsynchronized.ref([] : thm list);
 
 (*Return assumption list -- useful if you didn't save "goal"'s result. *)
 fun premises() = !curr_prems;
 
 (*Current result maker -- set by "goal", used by "result".  *)
 fun init_mkresult _ = error "No goal has been supplied in subgoal module";
-val curr_mkresult = ref (init_mkresult: bool*thm->thm);
+val curr_mkresult = Unsynchronized.ref (init_mkresult: bool*thm->thm);
 
 (*List of previous goal stacks, for the undo operation.  Set by setstate.
   A list of lists!*)
-val undo_list = ref([[(asm_rl, Seq.empty)]] : gstack list);
+val undo_list = Unsynchronized.ref([[(asm_rl, Seq.empty)]] : gstack list);
 
 (* Stack of proof attempts *)
-val proofstack = ref([]: proof list);
+val proofstack = Unsynchronized.ref([]: proof list);
 
 (*reset all refs*)
 fun reset_goals () =
@@ -272,7 +272,7 @@
       Goal_Display.pretty_goals_without_context (!goals_limit) state @
     [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
 
-val result_error_fn = ref result_error_default;
+val result_error_fn = Unsynchronized.ref result_error_default;
 
 
 (*Common treatment of "goal" and "prove_goal":
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/pattern.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -14,7 +14,7 @@
 
 signature PATTERN =
 sig
-  val trace_unify_fail: bool ref
+  val trace_unify_fail: bool Unsynchronized.ref
   val aeconv: term * term -> bool
   val eta_long: typ list -> term -> term
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -40,7 +40,7 @@
 exception Unif;
 exception Pattern;
 
-val trace_unify_fail = ref false;
+val trace_unify_fail = Unsynchronized.ref false;
 
 fun string_of_term thy env binders t =
   Syntax.string_of_term_global thy
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/proofterm.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -8,7 +8,7 @@
 
 signature BASIC_PROOFTERM =
 sig
-  val proofs: int ref
+  val proofs: int Unsynchronized.ref
 
   datatype proof =
      MinProof
@@ -885,7 +885,7 @@
 
 (***** axioms and theorems *****)
 
-val proofs = ref 2;
+val proofs = Unsynchronized.ref 2;
 
 fun vars_of t = map Var (rev (Term.add_vars t []));
 fun frees_of t = map Free (rev (Term.add_frees t []));
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/search.ML
--- a/src/Pure/search.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/search.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -13,23 +13,23 @@
   val THEN_MAYBE        : tactic * tactic -> tactic
   val THEN_MAYBE'       : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
 
-  val trace_DEPTH_FIRST : bool ref
+  val trace_DEPTH_FIRST : bool Unsynchronized.ref
   val DEPTH_FIRST       : (thm -> bool) -> tactic -> tactic
   val DEPTH_SOLVE       : tactic -> tactic
   val DEPTH_SOLVE_1     : tactic -> tactic
   val ITER_DEEPEN       : (thm->bool) -> (int->tactic) -> tactic
   val THEN_ITER_DEEPEN  : tactic -> (thm->bool) -> (int->tactic) -> tactic
-  val iter_deepen_limit : int ref
+  val iter_deepen_limit : int Unsynchronized.ref
 
   val has_fewer_prems   : int -> thm -> bool
   val IF_UNSOLVED       : tactic -> tactic
   val SOLVE             : tactic -> tactic
   val DETERM_UNTIL_SOLVED: tactic -> tactic
-  val trace_BEST_FIRST  : bool ref
+  val trace_BEST_FIRST  : bool Unsynchronized.ref
   val BEST_FIRST        : (thm -> bool) * (thm -> int) -> tactic -> tactic
   val THEN_BEST_FIRST   : tactic -> (thm->bool) * (thm->int) -> tactic
                           -> tactic
-  val trace_ASTAR       : bool ref
+  val trace_ASTAR       : bool Unsynchronized.ref
   val ASTAR             : (thm -> bool) * (int->thm->int) -> tactic -> tactic
   val THEN_ASTAR        : tactic -> (thm->bool) * (int->thm->int) -> tactic
                           -> tactic
@@ -50,7 +50,7 @@
 
 (**** Depth-first search ****)
 
-val trace_DEPTH_FIRST = ref false;
+val trace_DEPTH_FIRST = Unsynchronized.ref false;
 
 (*Searches until "satp" reports proof tree as satisfied.
   Suppresses duplicate solutions to minimize search space.*)
@@ -130,7 +130,7 @@
 
 
 (*No known example (on 1-5-2007) needs even thirty*)
-val iter_deepen_limit = ref 50;
+val iter_deepen_limit = Unsynchronized.ref 50;
 
 (*Depth-first iterative deepening search for a state that satisfies satp
   tactic tac0 sets up the initial goal queue, while tac1 searches it.
@@ -138,7 +138,7 @@
   to suppress solutions arising from earlier searches, as the accumulated cost
   (k) can be wrong.*)
 fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
- let val countr = ref 0
+ let val countr = Unsynchronized.ref 0
      and tf = tracify trace_DEPTH_FIRST (tac1 1)
      and qs0 = tac0 st
      (*bnd = depth bound; inc = estimate of increment required next*)
@@ -156,7 +156,7 @@
        | depth (bnd,inc) ((k,np,rgd,q)::qs) =
           if k>=bnd then depth (bnd,inc) qs
           else
-          case (countr := !countr+1;
+          case (Unsynchronized.inc countr;
                 if !trace_DEPTH_FIRST then
                     tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
                 else ();
@@ -199,7 +199,7 @@
 
 (*** Best-first search ***)
 
-val trace_BEST_FIRST = ref false;
+val trace_BEST_FIRST = Unsynchronized.ref false;
 
 (*For creating output sequence*)
 fun some_of_list []     = NONE
@@ -273,7 +273,7 @@
 fun some_of_list []     = NONE
   | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
 
-val trace_ASTAR = ref false;
+val trace_ASTAR = Unsynchronized.ref false;
 
 fun THEN_ASTAR tac0 (satp, costf) tac1 =
   let val tf = tracify trace_ASTAR tac1;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/simplifier.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -32,7 +32,7 @@
   include BASIC_SIMPLIFIER
   val pretty_ss: Proof.context -> simpset -> Pretty.T
   val clear_ss: simpset -> simpset
-  val debug_bounds: bool ref
+  val debug_bounds: bool Unsynchronized.ref
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
@@ -424,5 +424,5 @@
 
 end;
 
-structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
-open BasicSimplifier;
+structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
+open Basic_Simplifier;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/tactical.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -34,9 +34,9 @@
   val RANGE: (int -> tactic) list -> int -> tactic
   val print_tac: string -> tactic
   val pause_tac: tactic
-  val trace_REPEAT: bool ref
-  val suppress_tracing: bool ref
-  val tracify: bool ref -> tactic -> tactic
+  val trace_REPEAT: bool Unsynchronized.ref
+  val suppress_tracing: bool Unsynchronized.ref
+  val tracify: bool Unsynchronized.ref -> tactic -> tactic
   val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic
   val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic
   val REPEAT_DETERM_N: int -> tactic -> tactic
@@ -204,16 +204,16 @@
 and TRACE_QUIT;
 
 (*Tracing flags*)
-val trace_REPEAT= ref false
-and suppress_tracing = ref false;
+val trace_REPEAT= Unsynchronized.ref false
+and suppress_tracing = Unsynchronized.ref false;
 
 (*Handle all tracing commands for current state and tactic *)
 fun exec_trace_command flag (tac, st) =
    case TextIO.inputLine TextIO.stdIn of
        SOME "\n" => tac st
      | SOME "f\n" => Seq.empty
-     | SOME "o\n" => (flag:=false;  tac st)
-     | SOME "s\n" => (suppress_tracing:=true;  tac st)
+     | SOME "o\n" => (flag := false;  tac st)
+     | SOME "s\n" => (suppress_tracing := true;  tac st)
      | SOME "x\n" => (tracing "Exiting now";  raise (TRACE_EXIT st))
      | SOME "quit\n" => raise TRACE_QUIT
      | _     => (tracing
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/term.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -112,7 +112,7 @@
   val exists_type: (typ -> bool) -> term -> bool
   val exists_subterm: (term -> bool) -> term -> bool
   val exists_Const: (string * typ -> bool) -> term -> bool
-  val show_question_marks: bool ref
+  val show_question_marks: bool Unsynchronized.ref
 end;
 
 signature TERM =
@@ -963,7 +963,7 @@
 
 (* display variables *)
 
-val show_question_marks = ref true;
+val show_question_marks = Unsynchronized.ref true;
 
 fun string_of_vname (x, i) =
   let
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/term_subst.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -157,28 +157,32 @@
 in
 
 fun instantiateT_maxidx instT ty i =
-  let val maxidx = ref i
+  let val maxidx = Unsynchronized.ref i
   in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
 
 fun instantiate_maxidx insts tm i =
-  let val maxidx = ref i
+  let val maxidx = Unsynchronized.ref i
   in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
 
 fun instantiateT [] ty = ty
   | instantiateT instT ty =
-      (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle Same.SAME => ty);
+      (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
+        handle Same.SAME => ty);
 
 fun instantiate ([], []) tm = tm
   | instantiate insts tm =
-      (instantiate_same (ref ~1) (no_indexes2 insts) tm handle Same.SAME => tm);
+      (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
+        handle Same.SAME => tm);
 
 fun instantiateT_option [] _ = NONE
   | instantiateT_option instT ty =
-      (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle Same.SAME => NONE);
+      (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
+        handle Same.SAME => NONE);
 
 fun instantiate_option ([], []) _ = NONE
   | instantiate_option insts tm =
-      (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle Same.SAME => NONE);
+      (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
+        handle Same.SAME => NONE);
 
 end;
 
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/type.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -417,8 +417,8 @@
 (*order-sorted unification*)
 fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
   let
-    val tyvar_count = ref maxidx;
-    fun gen_tyvar S = TVar ((Name.aT, inc tyvar_count), S);
+    val tyvar_count = Unsynchronized.ref maxidx;
+    fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S);
 
     fun mg_domain a S = Sorts.mg_domain classes a S
       handle Sorts.CLASS_ERROR _ => raise TUNIFY;
diff -r 76fa673eee8b -r 15bb09ca0378 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/unify.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -106,7 +106,7 @@
   the occurs check must ignore the types of variables. This avoids
   that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
   substitution when ?'a is instantiated with T later. *)
-fun occurs_terms (seen: (indexname list) ref,
+fun occurs_terms (seen: (indexname list) Unsynchronized.ref,
       env: Envir.env, v: indexname, ts: term list): bool =
   let fun occurs [] = false
   | occurs (t::ts) =  occur t  orelse  occurs ts
@@ -160,7 +160,7 @@
 Warning: finds a rigid occurrence of ?f in ?f(t).
   Should NOT be called in this case: there is a flex-flex unifier
 *)
-fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
+fun rigid_occurs_term (seen: (indexname list) Unsynchronized.ref, env, v: indexname, t) =
   let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
            else NoOcc
       fun occurs [] = NoOcc
@@ -230,7 +230,7 @@
   If v occurs nonrigidly then must use full algorithm. *)
 fun assignment thy (env, rbinder, t, u) =
     let val vT as (v,T) = get_eta_var (rbinder, 0, t)
-    in  case rigid_occurs_term (ref [], env, v, u) of
+    in  case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
         NoOcc => let val env = unify_types thy (body_type env T,
              fastype env (rbinder,u),env)
     in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
@@ -429,7 +429,7 @@
   Attempts to update t with u, raising ASSIGN if impossible*)
 fun ff_assign thy (env, rbinder, t, u) : Envir.env =
 let val vT as (v,T) = get_eta_var(rbinder,0,t)
-in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
+in if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
    else let val env = unify_types thy (body_type env T,
           fastype env (rbinder,u),
           env)