explicit indication of Unsynchronized.ref;
authorwenzelm
Tue Sep 29 11:49:22 2009 +0200 (2009-09-29)
changeset 3273815bb09ca0378
parent 32737 76fa673eee8b
child 32739 31e75ad9ae17
explicit indication of Unsynchronized.ref;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/synchronized.ML
src/Pure/Concurrent/synchronized_dummy.ML
src/Pure/General/file.ML
src/Pure/General/lazy.ML
src/Pure/General/markup.ML
src/Pure/General/name_space.ML
src/Pure/General/output.ML
src/Pure/General/pretty.ML
src/Pure/General/print_mode.ML
src/Pure/General/secure.ML
src/Pure/Isar/code.ML
src/Pure/Isar/isar_document.ML
src/Pure/Isar/local_syntax.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_keyword.ML
src/Pure/Isar/outer_lex.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML-Systems/compiler_polyml-5.0.ML
src/Pure/ML-Systems/compiler_polyml-5.2.ML
src/Pure/ML-Systems/compiler_polyml-5.3.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML/ml_compiler_polyml-5.3.ML
src/Pure/ML/ml_context.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/reconstruct.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isar.ML
src/Pure/System/session.ML
src/Pure/Thy/html.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/find_theorems.ML
src/Pure/codegen.ML
src/Pure/context.ML
src/Pure/display.ML
src/Pure/goal.ML
src/Pure/goal_display.ML
src/Pure/meta_simplifier.ML
src/Pure/old_goals.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/search.ML
src/Pure/simplifier.ML
src/Pure/tactical.ML
src/Pure/term.ML
src/Pure/term_subst.ML
src/Pure/type.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -99,13 +99,13 @@
     1.4  
     1.5  (* global state *)
     1.6  
     1.7 -val queue = ref Task_Queue.empty;
     1.8 -val next = ref 0;
     1.9 -val workers = ref ([]: (Thread.thread * bool) list);
    1.10 -val scheduler = ref (NONE: Thread.thread option);
    1.11 -val excessive = ref 0;
    1.12 -val canceled = ref ([]: Task_Queue.group list);
    1.13 -val do_shutdown = ref false;
    1.14 +val queue = Unsynchronized.ref Task_Queue.empty;
    1.15 +val next = Unsynchronized.ref 0;
    1.16 +val workers = Unsynchronized.ref ([]: (Thread.thread * bool) list);
    1.17 +val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
    1.18 +val excessive = Unsynchronized.ref 0;
    1.19 +val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
    1.20 +val do_shutdown = Unsynchronized.ref false;
    1.21  
    1.22  
    1.23  (* synchronization *)
    1.24 @@ -162,7 +162,8 @@
    1.25    in (result, job) end;
    1.26  
    1.27  fun do_cancel group = (*requires SYNCHRONIZED*)
    1.28 - (change canceled (insert Task_Queue.eq_group group); broadcast scheduler_event);
    1.29 + (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
    1.30 +  broadcast scheduler_event);
    1.31  
    1.32  fun execute name (task, group, jobs) =
    1.33    let
    1.34 @@ -171,7 +172,7 @@
    1.35        fold (fn job => fn ok => job valid andalso ok) jobs true) ();
    1.36      val _ = SYNCHRONIZED "finish" (fn () =>
    1.37        let
    1.38 -        val maximal = change_result queue (Task_Queue.finish task);
    1.39 +        val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
    1.40          val _ =
    1.41            if ok then ()
    1.42            else if Task_Queue.cancel (! queue) group then ()
    1.43 @@ -188,7 +189,8 @@
    1.44    fold (fn (_, active) => fn i => if active then i + 1 else i) (! workers) 0;
    1.45  
    1.46  fun change_active active = (*requires SYNCHRONIZED*)
    1.47 -  change workers (AList.update Thread.equal (Thread.self (), active));
    1.48 +  Unsynchronized.change workers
    1.49 +    (AList.update Thread.equal (Thread.self (), active));
    1.50  
    1.51  
    1.52  (* worker threads *)
    1.53 @@ -198,14 +200,15 @@
    1.54  
    1.55  fun worker_next () = (*requires SYNCHRONIZED*)
    1.56    if ! excessive > 0 then
    1.57 -    (dec excessive;
    1.58 -     change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
    1.59 +    (Unsynchronized.dec excessive;
    1.60 +     Unsynchronized.change workers
    1.61 +      (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
    1.62       broadcast scheduler_event;
    1.63       NONE)
    1.64    else if count_active () > Multithreading.max_threads_value () then
    1.65      (worker_wait scheduler_event; worker_next ())
    1.66    else
    1.67 -    (case change_result queue (Task_Queue.dequeue (Thread.self ())) of
    1.68 +    (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of
    1.69        NONE => (worker_wait work_available; worker_next ())
    1.70      | some => some);
    1.71  
    1.72 @@ -215,13 +218,13 @@
    1.73    | SOME work => (execute name work; worker_loop name));
    1.74  
    1.75  fun worker_start name = (*requires SYNCHRONIZED*)
    1.76 -  change workers (cons (SimpleThread.fork false (fn () =>
    1.77 +  Unsynchronized.change workers (cons (SimpleThread.fork false (fn () =>
    1.78       (broadcast scheduler_event; worker_loop name)), true));
    1.79  
    1.80  
    1.81  (* scheduler *)
    1.82  
    1.83 -val last_status = ref Time.zeroTime;
    1.84 +val last_status = Unsynchronized.ref Time.zeroTime;
    1.85  val next_status = Time.fromMilliseconds 500;
    1.86  val next_round = Time.fromMilliseconds 50;
    1.87  
    1.88 @@ -263,7 +266,8 @@
    1.89      val _ = excessive := l - mm;
    1.90      val _ =
    1.91        if mm > l then
    1.92 -        funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
    1.93 +        funpow (mm - l) (fn () =>
    1.94 +          worker_start ("worker " ^ string_of_int (Unsynchronized.inc next))) ()
    1.95        else ();
    1.96  
    1.97      (*canceled groups*)
    1.98 @@ -272,7 +276,7 @@
    1.99        else
   1.100         (Multithreading.tracing 1 (fn () =>
   1.101            string_of_int (length (! canceled)) ^ " canceled groups");
   1.102 -        change canceled (filter_out (Task_Queue.cancel (! queue)));
   1.103 +        Unsynchronized.change canceled (filter_out (Task_Queue.cancel (! queue)));
   1.104          broadcast_work ());
   1.105  
   1.106      (*delay loop*)
   1.107 @@ -317,7 +321,8 @@
   1.108      val (result, job) = future_job group e;
   1.109      val task = SYNCHRONIZED "enqueue" (fn () =>
   1.110        let
   1.111 -        val (task, minimal) = change_result queue (Task_Queue.enqueue group deps pri job);
   1.112 +        val (task, minimal) =
   1.113 +          Unsynchronized.change_result queue (Task_Queue.enqueue group deps pri job);
   1.114          val _ = if minimal then signal work_available else ();
   1.115          val _ = scheduler_check ();
   1.116        in task end);
   1.117 @@ -347,7 +352,7 @@
   1.118  fun join_next deps = (*requires SYNCHRONIZED*)
   1.119    if null deps then NONE
   1.120    else
   1.121 -    (case change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
   1.122 +    (case Unsynchronized.change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
   1.123        (NONE, []) => NONE
   1.124      | (NONE, deps') => (worker_wait work_finished; join_next deps')
   1.125      | (SOME work, deps') => SOME (work, deps'));
     2.1 --- a/src/Pure/Concurrent/synchronized.ML	Tue Sep 29 11:48:32 2009 +0200
     2.2 +++ b/src/Pure/Concurrent/synchronized.ML	Tue Sep 29 11:49:22 2009 +0200
     2.3 @@ -24,13 +24,13 @@
     2.4   {name: string,
     2.5    lock: Mutex.mutex,
     2.6    cond: ConditionVar.conditionVar,
     2.7 -  var: 'a ref};
     2.8 +  var: 'a Unsynchronized.ref};
     2.9  
    2.10  fun var name x = Var
    2.11   {name = name,
    2.12    lock = Mutex.mutex (),
    2.13    cond = ConditionVar.conditionVar (),
    2.14 -  var = ref x};
    2.15 +  var = Unsynchronized.ref x};
    2.16  
    2.17  fun value (Var {var, ...}) = ! var;
    2.18  
     3.1 --- a/src/Pure/Concurrent/synchronized_dummy.ML	Tue Sep 29 11:48:32 2009 +0200
     3.2 +++ b/src/Pure/Concurrent/synchronized_dummy.ML	Tue Sep 29 11:49:22 2009 +0200
     3.3 @@ -7,9 +7,9 @@
     3.4  structure Synchronized: SYNCHRONIZED =
     3.5  struct
     3.6  
     3.7 -datatype 'a var = Var of 'a ref;
     3.8 +datatype 'a var = Var of 'a Unsynchronized.ref;
     3.9  
    3.10 -fun var _ x = Var (ref x);
    3.11 +fun var _ x = Var (Unsynchronized.ref x);
    3.12  fun value (Var var) = ! var;
    3.13  
    3.14  fun timed_access (Var var) _ f =
     4.1 --- a/src/Pure/General/file.ML	Tue Sep 29 11:48:32 2009 +0200
     4.2 +++ b/src/Pure/General/file.ML	Tue Sep 29 11:49:22 2009 +0200
     4.3 @@ -85,7 +85,8 @@
     4.4  (* file identification *)
     4.5  
     4.6  local
     4.7 -  val ident_cache = ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
     4.8 +  val ident_cache =
     4.9 +    Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
    4.10  in
    4.11  
    4.12  fun check_cache (path, time) = CRITICAL (fn () =>
    4.13 @@ -94,7 +95,8 @@
    4.14    | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
    4.15  
    4.16  fun update_cache (path, (time, id)) = CRITICAL (fn () =>
    4.17 -  change ident_cache (Symtab.update (path, {time_stamp = time, id = id})));
    4.18 +  Unsynchronized.change ident_cache
    4.19 +    (Symtab.update (path, {time_stamp = time, id = id})));
    4.20  
    4.21  end;
    4.22  
     5.1 --- a/src/Pure/General/lazy.ML	Tue Sep 29 11:48:32 2009 +0200
     5.2 +++ b/src/Pure/General/lazy.ML	Tue Sep 29 11:49:22 2009 +0200
     5.3 @@ -26,12 +26,12 @@
     5.4    Lazy of unit -> 'a |
     5.5    Result of 'a Exn.result;
     5.6  
     5.7 -type 'a lazy = 'a T ref;
     5.8 +type 'a lazy = 'a T Unsynchronized.ref;
     5.9  
    5.10  fun same (r1: 'a lazy, r2) = r1 = r2;
    5.11  
    5.12 -fun lazy e = ref (Lazy e);
    5.13 -fun value x = ref (Result (Exn.Result x));
    5.14 +fun lazy e = Unsynchronized.ref (Lazy e);
    5.15 +fun value x = Unsynchronized.ref (Result (Exn.Result x));
    5.16  
    5.17  fun peek r =
    5.18    (case ! r of
     6.1 --- a/src/Pure/General/markup.ML	Tue Sep 29 11:48:32 2009 +0200
     6.2 +++ b/src/Pure/General/markup.ML	Tue Sep 29 11:49:22 2009 +0200
     6.3 @@ -323,10 +323,10 @@
     6.4  
     6.5  local
     6.6    val default = {output = default_output};
     6.7 -  val modes = ref (Symtab.make [("", default)]);
     6.8 +  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
     6.9  in
    6.10    fun add_mode name output = CRITICAL (fn () =>
    6.11 -    change modes (Symtab.update_new (name, {output = output})));
    6.12 +    Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
    6.13    fun get_mode () =
    6.14      the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    6.15  end;
     7.1 --- a/src/Pure/General/name_space.ML	Tue Sep 29 11:48:32 2009 +0200
     7.2 +++ b/src/Pure/General/name_space.ML	Tue Sep 29 11:49:22 2009 +0200
     7.3 @@ -9,9 +9,9 @@
     7.4  
     7.5  signature BASIC_NAME_SPACE =
     7.6  sig
     7.7 -  val long_names: bool ref
     7.8 -  val short_names: bool ref
     7.9 -  val unique_names: bool ref
    7.10 +  val long_names: bool Unsynchronized.ref
    7.11 +  val short_names: bool Unsynchronized.ref
    7.12 +  val unique_names: bool Unsynchronized.ref
    7.13  end;
    7.14  
    7.15  signature NAME_SPACE =
    7.16 @@ -105,9 +105,9 @@
    7.17      else ext (get_accesses space name)
    7.18    end;
    7.19  
    7.20 -val long_names = ref false;
    7.21 -val short_names = ref false;
    7.22 -val unique_names = ref true;
    7.23 +val long_names = Unsynchronized.ref false;
    7.24 +val short_names = Unsynchronized.ref false;
    7.25 +val unique_names = Unsynchronized.ref true;
    7.26  
    7.27  fun extern space name =
    7.28    extern_flags
    7.29 @@ -261,6 +261,6 @@
    7.30  
    7.31  end;
    7.32  
    7.33 -structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
    7.34 -open BasicNameSpace;
    7.35 +structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
    7.36 +open Basic_Name_Space;
    7.37  
     8.1 --- a/src/Pure/General/output.ML	Tue Sep 29 11:48:32 2009 +0200
     8.2 +++ b/src/Pure/General/output.ML	Tue Sep 29 11:49:22 2009 +0200
     8.3 @@ -11,13 +11,13 @@
     8.4    val priority: string -> unit
     8.5    val tracing: string -> unit
     8.6    val warning: string -> unit
     8.7 -  val tolerate_legacy_features: bool ref
     8.8 +  val tolerate_legacy_features: bool Unsynchronized.ref
     8.9    val legacy_feature: string -> unit
    8.10    val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
    8.11    val timeit: (unit -> 'a) -> 'a
    8.12    val timeap: ('a -> 'b) -> 'a -> 'b
    8.13    val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
    8.14 -  val timing: bool ref
    8.15 +  val timing: bool Unsynchronized.ref
    8.16  end;
    8.17  
    8.18  signature OUTPUT =
    8.19 @@ -32,18 +32,18 @@
    8.20    val std_output: output -> unit
    8.21    val std_error: output -> unit
    8.22    val writeln_default: output -> unit
    8.23 -  val writeln_fn: (output -> unit) ref
    8.24 -  val priority_fn: (output -> unit) ref
    8.25 -  val tracing_fn: (output -> unit) ref
    8.26 -  val warning_fn: (output -> unit) ref
    8.27 -  val error_fn: (output -> unit) ref
    8.28 -  val debug_fn: (output -> unit) ref
    8.29 -  val prompt_fn: (output -> unit) ref
    8.30 -  val status_fn: (output -> unit) ref
    8.31 +  val writeln_fn: (output -> unit) Unsynchronized.ref
    8.32 +  val priority_fn: (output -> unit) Unsynchronized.ref
    8.33 +  val tracing_fn: (output -> unit) Unsynchronized.ref
    8.34 +  val warning_fn: (output -> unit) Unsynchronized.ref
    8.35 +  val error_fn: (output -> unit) Unsynchronized.ref
    8.36 +  val debug_fn: (output -> unit) Unsynchronized.ref
    8.37 +  val prompt_fn: (output -> unit) Unsynchronized.ref
    8.38 +  val status_fn: (output -> unit) Unsynchronized.ref
    8.39    val error_msg: string -> unit
    8.40    val prompt: string -> unit
    8.41    val status: string -> unit
    8.42 -  val debugging: bool ref
    8.43 +  val debugging: bool Unsynchronized.ref
    8.44    val no_warnings: ('a -> 'b) -> 'a -> 'b
    8.45    val debug: (unit -> string) -> unit
    8.46  end;
    8.47 @@ -60,10 +60,10 @@
    8.48  
    8.49  local
    8.50    val default = {output = default_output, escape = default_escape};
    8.51 -  val modes = ref (Symtab.make [("", default)]);
    8.52 +  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
    8.53  in
    8.54    fun add_mode name output escape = CRITICAL (fn () =>
    8.55 -    change modes (Symtab.update_new (name, {output = output, escape = escape})));
    8.56 +    Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
    8.57    fun get_mode () =
    8.58      the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    8.59  end;
    8.60 @@ -91,14 +91,14 @@
    8.61  
    8.62  (* Isabelle output channels *)
    8.63  
    8.64 -val writeln_fn = ref writeln_default;
    8.65 -val priority_fn = ref (fn s => ! writeln_fn s);
    8.66 -val tracing_fn = ref (fn s => ! writeln_fn s);
    8.67 -val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
    8.68 -val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
    8.69 -val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
    8.70 -val prompt_fn = ref std_output;
    8.71 -val status_fn = ref (fn _: string => ());
    8.72 +val writeln_fn = Unsynchronized.ref writeln_default;
    8.73 +val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    8.74 +val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    8.75 +val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
    8.76 +val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
    8.77 +val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
    8.78 +val prompt_fn = Unsynchronized.ref std_output;
    8.79 +val status_fn = Unsynchronized.ref (fn _: string => ());
    8.80  
    8.81  fun writeln s = ! writeln_fn (output s);
    8.82  fun priority s = ! priority_fn (output s);
    8.83 @@ -108,13 +108,13 @@
    8.84  fun prompt s = ! prompt_fn (output s);
    8.85  fun status s = ! status_fn (output s);
    8.86  
    8.87 -val tolerate_legacy_features = ref true;
    8.88 +val tolerate_legacy_features = Unsynchronized.ref true;
    8.89  fun legacy_feature s =
    8.90    (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
    8.91  
    8.92  fun no_warnings f = setmp warning_fn (K ()) f;
    8.93  
    8.94 -val debugging = ref false;
    8.95 +val debugging = Unsynchronized.ref false;
    8.96  fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
    8.97  
    8.98  
    8.99 @@ -140,9 +140,9 @@
   8.100  fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
   8.101  
   8.102  (*global timing mode*)
   8.103 -val timing = ref false;
   8.104 +val timing = Unsynchronized.ref false;
   8.105  
   8.106  end;
   8.107  
   8.108 -structure BasicOutput: BASIC_OUTPUT = Output;
   8.109 -open BasicOutput;
   8.110 +structure Basic_Output: BASIC_OUTPUT = Output;
   8.111 +open Basic_Output;
     9.1 --- a/src/Pure/General/pretty.ML	Tue Sep 29 11:48:32 2009 +0200
     9.2 +++ b/src/Pure/General/pretty.ML	Tue Sep 29 11:49:22 2009 +0200
     9.3 @@ -86,10 +86,10 @@
     9.4  
     9.5  local
     9.6    val default = {indent = default_indent};
     9.7 -  val modes = ref (Symtab.make [("", default)]);
     9.8 +  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
     9.9  in
    9.10    fun add_mode name indent = CRITICAL (fn () =>
    9.11 -    change modes (Symtab.update_new (name, {indent = indent})));
    9.12 +    Unsynchronized.change modes (Symtab.update_new (name, {indent = indent})));
    9.13    fun get_mode () =
    9.14      the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    9.15  end;
    9.16 @@ -186,14 +186,14 @@
    9.17    breakgain = m div 20,         (*minimum added space required of a break*)
    9.18    emergencypos = m div 2};      (*position too far to right*)
    9.19  
    9.20 -val margin_info = ref (make_margin_info 76);
    9.21 +val margin_info = Unsynchronized.ref (make_margin_info 76);
    9.22  fun setmargin m = margin_info := make_margin_info m;
    9.23  fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
    9.24  
    9.25  
    9.26  (* depth limitation *)
    9.27  
    9.28 -val depth = ref 0;   (*maximum depth; 0 means no limit*)
    9.29 +val depth = Unsynchronized.ref 0;   (*maximum depth; 0 means no limit*)
    9.30  fun setdepth dp = (depth := dp);
    9.31  
    9.32  local
    10.1 --- a/src/Pure/General/print_mode.ML	Tue Sep 29 11:48:32 2009 +0200
    10.2 +++ b/src/Pure/General/print_mode.ML	Tue Sep 29 11:49:22 2009 +0200
    10.3 @@ -7,9 +7,9 @@
    10.4  
    10.5  signature BASIC_PRINT_MODE =
    10.6  sig
    10.7 -  val print_mode: string list ref            (*global template*)
    10.8 -  val print_mode_value: unit -> string list  (*thread-local value*)
    10.9 -  val print_mode_active: string -> bool      (*thread-local value*)
   10.10 +  val print_mode: string list Unsynchronized.ref  (*global template*)
   10.11 +  val print_mode_value: unit -> string list       (*thread-local value*)
   10.12 +  val print_mode_active: string -> bool           (*thread-local value*)
   10.13  end;
   10.14  
   10.15  signature PRINT_MODE =
   10.16 @@ -28,7 +28,7 @@
   10.17  val input = "input";
   10.18  val internal = "internal";
   10.19  
   10.20 -val print_mode = ref ([]: string list);
   10.21 +val print_mode = Unsynchronized.ref ([]: string list);
   10.22  val tag = Universal.tag () : string list option Universal.tag;
   10.23  
   10.24  fun print_mode_value () =
    11.1 --- a/src/Pure/General/secure.ML	Tue Sep 29 11:48:32 2009 +0200
    11.2 +++ b/src/Pure/General/secure.ML	Tue Sep 29 11:49:22 2009 +0200
    11.3 @@ -23,7 +23,7 @@
    11.4  
    11.5  (** secure flag **)
    11.6  
    11.7 -val secure = ref false;
    11.8 +val secure = Unsynchronized.ref false;
    11.9  
   11.10  fun set_secure () = secure := true;
   11.11  fun is_secure () = ! secure;
    12.1 --- a/src/Pure/Isar/code.ML	Tue Sep 29 11:48:32 2009 +0200
    12.2 +++ b/src/Pure/Isar/code.ML	Tue Sep 29 11:49:22 2009 +0200
    12.3 @@ -217,8 +217,8 @@
    12.4    purge: theory -> string list -> Object.T -> Object.T
    12.5  };
    12.6  
    12.7 -val kinds = ref (Datatab.empty: kind Datatab.table);
    12.8 -val kind_keys = ref ([]: serial list);
    12.9 +val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
   12.10 +val kind_keys = Unsynchronized.ref ([]: serial list);
   12.11  
   12.12  fun invoke f k = case Datatab.lookup (! kinds) k
   12.13   of SOME kind => f kind
   12.14 @@ -230,8 +230,8 @@
   12.15    let
   12.16      val k = serial ();
   12.17      val kind = {empty = empty, purge = purge};
   12.18 -    val _ = change kinds (Datatab.update (k, kind));
   12.19 -    val _ = change kind_keys (cons k);
   12.20 +    val _ = Unsynchronized.change kinds (Datatab.update (k, kind));
   12.21 +    val _ = Unsynchronized.change kind_keys (cons k);
   12.22    in k end;
   12.23  
   12.24  fun invoke_init k = invoke (fn kind => #empty kind) k;
   12.25 @@ -252,13 +252,13 @@
   12.26  
   12.27  structure Code_Data = TheoryDataFun
   12.28  (
   12.29 -  type T = spec * data ref;
   12.30 +  type T = spec * data Unsynchronized.ref;
   12.31    val empty = (make_spec (false,
   12.32 -    (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), ref empty_data);
   12.33 -  fun copy (spec, data) = (spec, ref (! data));
   12.34 +    (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
   12.35 +  fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
   12.36    val extend = copy;
   12.37    fun merge pp ((spec1, data1), (spec2, data2)) =
   12.38 -    (merge_spec (spec1, spec2), ref empty_data);
   12.39 +    (merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
   12.40  );
   12.41  
   12.42  fun thy_data f thy = f ((snd o Code_Data.get) thy);
   12.43 @@ -267,7 +267,7 @@
   12.44    case Datatab.lookup (! data_ref) kind
   12.45     of SOME x => x
   12.46      | NONE => let val y = invoke_init kind
   12.47 -        in (change data_ref (Datatab.update (kind, y)); y) end;
   12.48 +        in (Unsynchronized.change data_ref (Datatab.update (kind, y)); y) end;
   12.49  
   12.50  in
   12.51  
   12.52 @@ -281,11 +281,11 @@
   12.53      | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
   12.54  
   12.55  fun map_exec_purge touched f thy =
   12.56 -  Code_Data.map (fn (exec, data) => (f exec, ref (case touched
   12.57 +  Code_Data.map (fn (exec, data) => (f exec, Unsynchronized.ref (case touched
   12.58     of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
   12.59      | NONE => empty_data))) thy;
   12.60  
   12.61 -val purge_data = (Code_Data.map o apsnd) (K (ref empty_data));
   12.62 +val purge_data = (Code_Data.map o apsnd) (K (Unsynchronized.ref empty_data));
   12.63  
   12.64  fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
   12.65    o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
   12.66 @@ -332,7 +332,7 @@
   12.67        let
   12.68          val data = get_ensure_init kind data_ref;
   12.69          val data' = f (dest data);
   12.70 -      in (change data_ref (Datatab.update (kind, mk data')); data') end;
   12.71 +      in (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
   12.72    in thy_data chnge end;
   12.73  
   12.74  fun change_yield_data (kind, mk, dest) =
   12.75 @@ -341,7 +341,7 @@
   12.76        let
   12.77          val data = get_ensure_init kind data_ref;
   12.78          val (x, data') = f (dest data);
   12.79 -      in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end;
   12.80 +      in (x, (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
   12.81    in thy_data chnge end;
   12.82  
   12.83  end; (*local*)
    13.1 --- a/src/Pure/Isar/isar_document.ML	Tue Sep 29 11:48:32 2009 +0200
    13.2 +++ b/src/Pure/Isar/isar_document.ML	Tue Sep 29 11:49:22 2009 +0200
    13.3 @@ -112,18 +112,18 @@
    13.4  (** global configuration **)
    13.5  
    13.6  local
    13.7 -  val global_states = ref (Symtab.empty: Toplevel.state option future Symtab.table);
    13.8 -  val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
    13.9 -  val global_documents = ref (Symtab.empty: document Symtab.table);
   13.10 +  val global_states = Unsynchronized.ref (Symtab.empty: Toplevel.state option future Symtab.table);
   13.11 +  val global_commands = Unsynchronized.ref (Symtab.empty: Toplevel.transition Symtab.table);
   13.12 +  val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
   13.13  in
   13.14  
   13.15 -fun change_states f = NAMED_CRITICAL "Isar" (fn () => change global_states f);
   13.16 +fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
   13.17  fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
   13.18  
   13.19 -fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
   13.20 +fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
   13.21  fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
   13.22  
   13.23 -fun change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
   13.24 +fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
   13.25  fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
   13.26  
   13.27  fun init () = NAMED_CRITICAL "Isar" (fn () =>
    14.1 --- a/src/Pure/Isar/local_syntax.ML	Tue Sep 29 11:48:32 2009 +0200
    14.2 +++ b/src/Pure/Isar/local_syntax.ML	Tue Sep 29 11:49:22 2009 +0200
    14.3 @@ -4,7 +4,7 @@
    14.4  Local syntax depending on theory syntax.
    14.5  *)
    14.6  
    14.7 -val show_structs = ref false;
    14.8 +val show_structs = Unsynchronized.ref false;
    14.9  
   14.10  signature LOCAL_SYNTAX =
   14.11  sig
    15.1 --- a/src/Pure/Isar/method.ML	Tue Sep 29 11:48:32 2009 +0200
    15.2 +++ b/src/Pure/Isar/method.ML	Tue Sep 29 11:49:22 2009 +0200
    15.3 @@ -8,7 +8,7 @@
    15.4  sig
    15.5    val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
    15.6    val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
    15.7 -  val trace_rules: bool ref
    15.8 +  val trace_rules: bool Unsynchronized.ref
    15.9  end;
   15.10  
   15.11  signature METHOD =
   15.12 @@ -215,7 +215,7 @@
   15.13  
   15.14  (* rule etc. -- single-step refinements *)
   15.15  
   15.16 -val trace_rules = ref false;
   15.17 +val trace_rules = Unsynchronized.ref false;
   15.18  
   15.19  fun trace ctxt rules =
   15.20    if ! trace_rules andalso not (null rules) then
    16.1 --- a/src/Pure/Isar/outer_keyword.ML	Tue Sep 29 11:48:32 2009 +0200
    16.2 +++ b/src/Pure/Isar/outer_keyword.ML	Tue Sep 29 11:49:22 2009 +0200
    16.3 @@ -116,16 +116,16 @@
    16.4  
    16.5  local
    16.6  
    16.7 -val global_commands = ref (Symtab.empty: T Symtab.table);
    16.8 -val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
    16.9 +val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
   16.10 +val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
   16.11  
   16.12  in
   16.13  
   16.14  fun get_commands () = CRITICAL (fn () => ! global_commands);
   16.15  fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
   16.16  
   16.17 -fun change_commands f = CRITICAL (fn () => change global_commands f);
   16.18 -fun change_lexicons f = CRITICAL (fn () => change global_lexicons f);
   16.19 +fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
   16.20 +fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
   16.21  
   16.22  end;
   16.23  
    17.1 --- a/src/Pure/Isar/outer_lex.ML	Tue Sep 29 11:48:32 2009 +0200
    17.2 +++ b/src/Pure/Isar/outer_lex.ML	Tue Sep 29 11:49:22 2009 +0200
    17.3 @@ -83,7 +83,7 @@
    17.4  datatype slot =
    17.5    Slot |
    17.6    Value of value option |
    17.7 -  Assignable of value option ref;
    17.8 +  Assignable of value option Unsynchronized.ref;
    17.9  
   17.10  
   17.11  (* datatype token *)
   17.12 @@ -245,7 +245,7 @@
   17.13  (* static binding *)
   17.14  
   17.15  (*1st stage: make empty slots assignable*)
   17.16 -fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (ref NONE))
   17.17 +fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
   17.18    | assignable tok = tok;
   17.19  
   17.20  (*2nd stage: assign values as side-effect of scanning*)
   17.21 @@ -253,7 +253,7 @@
   17.22    | assign _ _ = ();
   17.23  
   17.24  (*3rd stage: static closure of final values*)
   17.25 -fun closure (Token (x, y, Assignable (ref v))) = Token (x, y, Value v)
   17.26 +fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
   17.27    | closure tok = tok;
   17.28  
   17.29  
    18.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 29 11:48:32 2009 +0200
    18.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 29 11:49:22 2009 +0200
    18.3 @@ -88,11 +88,11 @@
    18.4  
    18.5  local
    18.6  
    18.7 -val global_commands = ref (Symtab.empty: command Symtab.table);
    18.8 -val global_markups = ref ([]: (string * ThyOutput.markup) list);
    18.9 +val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
   18.10 +val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
   18.11  
   18.12  fun change_commands f = CRITICAL (fn () =>
   18.13 - (change global_commands f;
   18.14 + (Unsynchronized.change global_commands f;
   18.15    global_markups :=
   18.16      Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
   18.17        (! global_commands) []));
    19.1 --- a/src/Pure/Isar/proof.ML	Tue Sep 29 11:48:32 2009 +0200
    19.2 +++ b/src/Pure/Isar/proof.ML	Tue Sep 29 11:49:22 2009 +0200
    19.3 @@ -30,8 +30,8 @@
    19.4    val enter_forward: state -> state
    19.5    val goal_message: (unit -> Pretty.T) -> state -> state
    19.6    val get_goal: state -> context * (thm list * thm)
    19.7 -  val show_main_goal: bool ref
    19.8 -  val verbose: bool ref
    19.9 +  val show_main_goal: bool Unsynchronized.ref
   19.10 +  val verbose: bool Unsynchronized.ref
   19.11    val pretty_state: int -> state -> Pretty.T list
   19.12    val pretty_goals: bool -> state -> Pretty.T list
   19.13    val refine: Method.text -> state -> state Seq.seq
   19.14 @@ -315,7 +315,7 @@
   19.15  
   19.16  (** pretty_state **)
   19.17  
   19.18 -val show_main_goal = ref false;
   19.19 +val show_main_goal = Unsynchronized.ref false;
   19.20  val verbose = ProofContext.verbose;
   19.21  
   19.22  fun pretty_facts _ _ NONE = []
   19.23 @@ -930,8 +930,8 @@
   19.24  
   19.25  fun gen_show prep_att prepp before_qed after_qed stmt int state =
   19.26    let
   19.27 -    val testing = ref false;
   19.28 -    val rule = ref (NONE: thm option);
   19.29 +    val testing = Unsynchronized.ref false;
   19.30 +    val rule = Unsynchronized.ref (NONE: thm option);
   19.31      fun fail_msg ctxt =
   19.32        "Local statement will fail to refine any pending goal" ::
   19.33        (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
    20.1 --- a/src/Pure/Isar/proof_context.ML	Tue Sep 29 11:48:32 2009 +0200
    20.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Sep 29 11:49:22 2009 +0200
    20.3 @@ -123,15 +123,15 @@
    20.4    val add_abbrev: string -> Properties.T ->
    20.5      binding * term -> Proof.context -> (term * term) * Proof.context
    20.6    val revert_abbrev: string -> string -> Proof.context -> Proof.context
    20.7 -  val verbose: bool ref
    20.8 +  val verbose: bool Unsynchronized.ref
    20.9    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   20.10    val print_syntax: Proof.context -> unit
   20.11    val print_abbrevs: Proof.context -> unit
   20.12    val print_binds: Proof.context -> unit
   20.13    val print_lthms: Proof.context -> unit
   20.14    val print_cases: Proof.context -> unit
   20.15 -  val debug: bool ref
   20.16 -  val prems_limit: int ref
   20.17 +  val debug: bool Unsynchronized.ref
   20.18 +  val prems_limit: int Unsynchronized.ref
   20.19    val pretty_ctxt: Proof.context -> Pretty.T list
   20.20    val pretty_context: Proof.context -> Pretty.T list
   20.21    val query_type: Proof.context -> string -> Properties.T
   20.22 @@ -1208,9 +1208,9 @@
   20.23  
   20.24  (** print context information **)
   20.25  
   20.26 -val debug = ref false;
   20.27 +val debug = Unsynchronized.ref false;
   20.28  
   20.29 -val verbose = ref false;
   20.30 +val verbose = Unsynchronized.ref false;
   20.31  fun verb f x = if ! verbose then f (x ()) else [];
   20.32  
   20.33  fun setmp_verbose f x = Library.setmp verbose true f x;
   20.34 @@ -1320,7 +1320,7 @@
   20.35  
   20.36  (* core context *)
   20.37  
   20.38 -val prems_limit = ref ~1;
   20.39 +val prems_limit = Unsynchronized.ref ~1;
   20.40  
   20.41  fun pretty_ctxt ctxt =
   20.42    if ! prems_limit < 0 andalso not (! debug) then []
    21.1 --- a/src/Pure/Isar/toplevel.ML	Tue Sep 29 11:48:32 2009 +0200
    21.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Sep 29 11:49:22 2009 +0200
    21.3 @@ -24,12 +24,12 @@
    21.4    val enter_proof_body: state -> Proof.state
    21.5    val print_state_context: state -> unit
    21.6    val print_state: bool -> state -> unit
    21.7 -  val quiet: bool ref
    21.8 -  val debug: bool ref
    21.9 -  val interact: bool ref
   21.10 -  val timing: bool ref
   21.11 -  val profiling: int ref
   21.12 -  val skip_proofs: bool ref
   21.13 +  val quiet: bool Unsynchronized.ref
   21.14 +  val debug: bool Unsynchronized.ref
   21.15 +  val interact: bool Unsynchronized.ref
   21.16 +  val timing: bool Unsynchronized.ref
   21.17 +  val profiling: int Unsynchronized.ref
   21.18 +  val skip_proofs: bool Unsynchronized.ref
   21.19    exception TERMINATE
   21.20    exception TOPLEVEL_ERROR
   21.21    val program: (unit -> 'a) -> 'a
   21.22 @@ -216,12 +216,12 @@
   21.23  
   21.24  (** toplevel transitions **)
   21.25  
   21.26 -val quiet = ref false;
   21.27 +val quiet = Unsynchronized.ref false;
   21.28  val debug = Output.debugging;
   21.29 -val interact = ref false;
   21.30 +val interact = Unsynchronized.ref false;
   21.31  val timing = Output.timing;
   21.32 -val profiling = ref 0;
   21.33 -val skip_proofs = ref false;
   21.34 +val profiling = Unsynchronized.ref 0;
   21.35 +val skip_proofs = Unsynchronized.ref false;
   21.36  
   21.37  exception TERMINATE = Runtime.TERMINATE;
   21.38  exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
   21.39 @@ -550,9 +550,9 @@
   21.40  
   21.41  (* post-transition hooks *)
   21.42  
   21.43 -local val hooks = ref ([]: (transition -> state -> state -> unit) list) in
   21.44 +local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
   21.45  
   21.46 -fun add_hook f = CRITICAL (fn () => change hooks (cons f));
   21.47 +fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
   21.48  fun get_hooks () = CRITICAL (fn () => ! hooks);
   21.49  
   21.50  end;
    22.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Tue Sep 29 11:48:32 2009 +0200
    22.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Tue Sep 29 11:49:22 2009 +0200
    22.3 @@ -5,11 +5,11 @@
    22.4  
    22.5  fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
    22.6    let
    22.7 -    val in_buffer = ref (explode (tune_source txt));
    22.8 -    val out_buffer = ref ([]: string list);
    22.9 +    val in_buffer = Unsynchronized.ref (explode (tune_source txt));
   22.10 +    val out_buffer = Unsynchronized.ref ([]: string list);
   22.11      fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
   22.12  
   22.13 -    val current_line = ref line;
   22.14 +    val current_line = Unsynchronized.ref line;
   22.15      fun get () =
   22.16        (case ! in_buffer of
   22.17          [] => ""
    23.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Tue Sep 29 11:48:32 2009 +0200
    23.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Tue Sep 29 11:49:22 2009 +0200
    23.3 @@ -14,9 +14,9 @@
    23.4  fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    23.5      (start_line, name) verbose txt =
    23.6    let
    23.7 -    val current_line = ref start_line;
    23.8 -    val in_buffer = ref (String.explode (tune_source txt));
    23.9 -    val out_buffer = ref ([]: string list);
   23.10 +    val current_line = Unsynchronized.ref start_line;
   23.11 +    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
   23.12 +    val out_buffer = Unsynchronized.ref ([]: string list);
   23.13      fun output () = drop_newline (implode (rev (! out_buffer)));
   23.14  
   23.15      fun get () =
    24.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Tue Sep 29 11:48:32 2009 +0200
    24.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Tue Sep 29 11:49:22 2009 +0200
    24.3 @@ -14,9 +14,9 @@
    24.4  fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    24.5      (start_line, name) verbose txt =
    24.6    let
    24.7 -    val line = ref start_line;
    24.8 -    val in_buffer = ref (String.explode (tune_source txt));
    24.9 -    val out_buffer = ref ([]: string list);
   24.10 +    val line = Unsynchronized.ref start_line;
   24.11 +    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
   24.12 +    val out_buffer = Unsynchronized.ref ([]: string list);
   24.13      fun output () = drop_newline (implode (rev (! out_buffer)));
   24.14  
   24.15      fun get () =
    25.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 29 11:48:32 2009 +0200
    25.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 29 11:49:22 2009 +0200
    25.3 @@ -31,7 +31,7 @@
    25.4  
    25.5  val available = true;
    25.6  
    25.7 -val max_threads = ref 0;
    25.8 +val max_threads = Unsynchronized.ref 0;
    25.9  
   25.10  val tested_platform =
   25.11    let val ml_platform = getenv "ML_PLATFORM"
   25.12 @@ -114,7 +114,7 @@
   25.13  
   25.14  (* tracing *)
   25.15  
   25.16 -val trace = ref 0;
   25.17 +val trace = Unsynchronized.ref 0;
   25.18  
   25.19  fun tracing level msg =
   25.20    if level > ! trace then ()
   25.21 @@ -148,7 +148,7 @@
   25.22  fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
   25.23    let
   25.24      val worker = Thread.self ();
   25.25 -    val timeout = ref false;
   25.26 +    val timeout = Unsynchronized.ref false;
   25.27      val watchdog = Thread.fork (fn () =>
   25.28        (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
   25.29  
   25.30 @@ -173,7 +173,7 @@
   25.31  
   25.32      (*result state*)
   25.33      datatype result = Wait | Signal | Result of int;
   25.34 -    val result = ref Wait;
   25.35 +    val result = Unsynchronized.ref Wait;
   25.36      val lock = Mutex.mutex ();
   25.37      val cond = ConditionVar.conditionVar ();
   25.38      fun set_result res =
   25.39 @@ -231,8 +231,8 @@
   25.40  local
   25.41  
   25.42  val critical_lock = Mutex.mutex ();
   25.43 -val critical_thread = ref (NONE: Thread.thread option);
   25.44 -val critical_name = ref "";
   25.45 +val critical_thread = Unsynchronized.ref (NONE: Thread.thread option);
   25.46 +val critical_name = Unsynchronized.ref "";
   25.47  
   25.48  in
   25.49  
   25.50 @@ -274,7 +274,7 @@
   25.51  local
   25.52  
   25.53  val serial_lock = Mutex.mutex ();
   25.54 -val serial_count = ref 0;
   25.55 +val serial_count = Unsynchronized.ref 0;
   25.56  
   25.57  in
   25.58  
    26.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 29 11:48:32 2009 +0200
    26.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 29 11:49:22 2009 +0200
    26.3 @@ -91,8 +91,8 @@
    26.4        if null toks then Position.none
    26.5        else ML_Lex.end_pos_of (List.last toks);
    26.6  
    26.7 -    val input_buffer = ref (input @ [(offset_of end_pos, #"\n")]);
    26.8 -    val line = ref (the_default 1 (Position.line_of pos));
    26.9 +    val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
   26.10 +    val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
   26.11  
   26.12      fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
   26.13      fun get () =
   26.14 @@ -106,9 +106,9 @@
   26.15  
   26.16      (* output *)
   26.17  
   26.18 -    val output_buffer = ref Buffer.empty;
   26.19 +    val output_buffer = Unsynchronized.ref Buffer.empty;
   26.20      fun output () = Buffer.content (! output_buffer);
   26.21 -    fun put s = change output_buffer (Buffer.add s);
   26.22 +    fun put s = Unsynchronized.change output_buffer (Buffer.add s);
   26.23  
   26.24      fun put_message {message, hard, location, context = _} =
   26.25       (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");
    27.1 --- a/src/Pure/ML/ml_context.ML	Tue Sep 29 11:48:32 2009 +0200
    27.2 +++ b/src/Pure/ML/ml_context.ML	Tue Sep 29 11:49:22 2009 +0200
    27.3 @@ -19,20 +19,21 @@
    27.4    val the_global_context: unit -> theory
    27.5    val the_local_context: unit -> Proof.context
    27.6    val exec: (unit -> unit) -> Context.generic -> Context.generic
    27.7 -  val stored_thms: thm list ref
    27.8 +  val stored_thms: thm list Unsynchronized.ref
    27.9    val ml_store_thm: string * thm -> unit
   27.10    val ml_store_thms: string * thm list -> unit
   27.11    type antiq =
   27.12      {struct_name: string, background: Proof.context} ->
   27.13        (Proof.context -> string * string) * Proof.context
   27.14    val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
   27.15 -  val trace: bool ref
   27.16 +  val trace: bool Unsynchronized.ref
   27.17    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
   27.18      Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   27.19    val eval: bool -> Position.T -> Symbol_Pos.text -> unit
   27.20    val eval_file: Path.T -> unit
   27.21    val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
   27.22 -  val evaluate: Proof.context -> bool -> string * (unit -> 'a) option ref -> string -> 'a
   27.23 +  val evaluate: Proof.context -> bool ->
   27.24 +    string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
   27.25    val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
   27.26  end
   27.27  
   27.28 @@ -53,7 +54,7 @@
   27.29  
   27.30  (* theorem bindings *)
   27.31  
   27.32 -val stored_thms: thm list ref = ref [];
   27.33 +val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref [];
   27.34  
   27.35  fun ml_store sel (name, ths) =
   27.36    let
   27.37 @@ -89,12 +90,13 @@
   27.38  
   27.39  local
   27.40  
   27.41 -val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
   27.42 +val global_parsers =
   27.43 +  Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
   27.44  
   27.45  in
   27.46  
   27.47  fun add_antiq name scan = CRITICAL (fn () =>
   27.48 -  change global_parsers (fn tab =>
   27.49 +  Unsynchronized.change global_parsers (fn tab =>
   27.50     (if not (Symtab.defined tab name) then ()
   27.51      else warning ("Redefined ML antiquotation: " ^ quote name);
   27.52      Symtab.update (name, scan) tab)));
   27.53 @@ -162,7 +164,7 @@
   27.54          in (ml, SOME (Context.Proof ctxt')) end;
   27.55    in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
   27.56  
   27.57 -val trace = ref false;
   27.58 +val trace = Unsynchronized.ref false;
   27.59  
   27.60  fun eval verbose pos txt =
   27.61    let
    28.1 --- a/src/Pure/Proof/extraction.ML	Tue Sep 29 11:48:32 2009 +0200
    28.2 +++ b/src/Pure/Proof/extraction.ML	Tue Sep 29 11:49:22 2009 +0200
    28.3 @@ -91,7 +91,7 @@
    28.4        Pattern.rewrite_term thy [] (condrew' :: procs) tm
    28.5      and condrew' tm =
    28.6        let
    28.7 -        val cache = ref ([] : (term * term) list);
    28.8 +        val cache = Unsynchronized.ref ([] : (term * term) list);
    28.9          fun lookup f x = (case AList.lookup (op =) (!cache) x of
   28.10              NONE =>
   28.11                let val y = f x
    29.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Sep 29 11:48:32 2009 +0200
    29.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Sep 29 11:49:22 2009 +0200
    29.3 @@ -6,7 +6,7 @@
    29.4  
    29.5  signature RECONSTRUCT =
    29.6  sig
    29.7 -  val quiet_mode : bool ref
    29.8 +  val quiet_mode : bool Unsynchronized.ref
    29.9    val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
   29.10    val prop_of' : term list -> Proofterm.proof -> term
   29.11    val prop_of : Proofterm.proof -> term
   29.12 @@ -19,7 +19,7 @@
   29.13  
   29.14  open Proofterm;
   29.15  
   29.16 -val quiet_mode = ref true;
   29.17 +val quiet_mode = Unsynchronized.ref true;
   29.18  fun message s = if !quiet_mode then () else writeln s;
   29.19  
   29.20  fun vars_of t = map Var (rev (Term.add_vars t []));
    30.1 --- a/src/Pure/ProofGeneral/preferences.ML	Tue Sep 29 11:48:32 2009 +0200
    30.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Tue Sep 29 11:49:22 2009 +0200
    30.3 @@ -18,11 +18,11 @@
    30.4      get: unit -> string,
    30.5      set: string -> unit}
    30.6    val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
    30.7 -    'a ref -> string -> string -> preference
    30.8 -  val string_pref: string ref -> string -> string -> preference
    30.9 -  val int_pref: int ref -> string -> string -> preference
   30.10 -  val nat_pref: int ref -> string -> string -> preference
   30.11 -  val bool_pref: bool ref -> string -> string -> preference
   30.12 +    'a Unsynchronized.ref -> string -> string -> preference
   30.13 +  val string_pref: string Unsynchronized.ref -> string -> string -> preference
   30.14 +  val int_pref: int Unsynchronized.ref -> string -> string -> preference
   30.15 +  val nat_pref: int Unsynchronized.ref -> string -> string -> preference
   30.16 +  val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
   30.17    type T = (string * preference list) list
   30.18    val pure_preferences: T
   30.19    val remove: string -> T -> T
   30.20 @@ -95,8 +95,9 @@
   30.21    let
   30.22      fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
   30.23      fun set s =
   30.24 -      if PgipTypes.read_pgipbool s then change print_mode (insert (op =) thm_depsN)
   30.25 -      else change print_mode (remove (op =) thm_depsN);
   30.26 +      if PgipTypes.read_pgipbool s
   30.27 +      then Unsynchronized.change print_mode (insert (op =) thm_depsN)
   30.28 +      else Unsynchronized.change print_mode (remove (op =) thm_depsN);
   30.29    in
   30.30      mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
   30.31        "Track theorem dependencies within Proof General"
    31.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 29 11:48:32 2009 +0200
    31.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 29 11:49:22 2009 +0200
    31.3 @@ -226,7 +226,7 @@
    31.4  
    31.5  (* init *)
    31.6  
    31.7 -val initialized = ref false;
    31.8 +val initialized = Unsynchronized.ref false;
    31.9  
   31.10  fun init false = panic "No Proof General interface support for Isabelle/classic mode."
   31.11    | init true =
   31.12 @@ -239,9 +239,9 @@
   31.13            ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
   31.14            setup_thy_loader ();
   31.15            setup_present_hook ();
   31.16 -          set initialized);
   31.17 +          Unsynchronized.set initialized);
   31.18          sync_thy_loader ();
   31.19 -       change print_mode (update (op =) proof_generalN);
   31.20 +       Unsynchronized.change print_mode (update (op =) proof_generalN);
   31.21         Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
   31.22  
   31.23  end;
    32.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 29 11:48:32 2009 +0200
    32.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 29 11:49:22 2009 +0200
    32.3 @@ -32,20 +32,20 @@
    32.4  (** print mode **)
    32.5  
    32.6  val proof_generalN = "ProofGeneral";
    32.7 -val pgmlsymbols_flag = ref true;
    32.8 +val pgmlsymbols_flag = Unsynchronized.ref true;
    32.9  
   32.10  
   32.11  (* assembling and issuing PGIP packets *)
   32.12  
   32.13 -val pgip_refid = ref NONE: string option ref;
   32.14 -val pgip_refseq = ref NONE: int option ref;
   32.15 +val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
   32.16 +val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
   32.17  
   32.18  local
   32.19    val pgip_class  = "pg"
   32.20    val pgip_tag = "Isabelle/Isar"
   32.21 -  val pgip_id = ref ""
   32.22 -  val pgip_seq = ref 0
   32.23 -  fun pgip_serial () = inc pgip_seq
   32.24 +  val pgip_id = Unsynchronized.ref ""
   32.25 +  val pgip_seq = Unsynchronized.ref 0
   32.26 +  fun pgip_serial () = Unsynchronized.inc pgip_seq
   32.27  
   32.28    fun assemble_pgips pgips =
   32.29      Pgip { tag = SOME pgip_tag,
   32.30 @@ -65,7 +65,7 @@
   32.31  
   32.32  fun matching_pgip_id id = (id = ! pgip_id)
   32.33  
   32.34 -val output_xml_fn = ref Output.writeln_default
   32.35 +val output_xml_fn = Unsynchronized.ref Output.writeln_default
   32.36  fun output_xml s = ! output_xml_fn (XML.string_of s);
   32.37  
   32.38  val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
   32.39 @@ -280,7 +280,7 @@
   32.40  
   32.41  (* theorem dependeny output *)
   32.42  
   32.43 -val show_theorem_dependencies = ref false;
   32.44 +val show_theorem_dependencies = Unsynchronized.ref false;
   32.45  
   32.46  local
   32.47  
   32.48 @@ -368,13 +368,13 @@
   32.49  
   32.50  (* Preferences: tweak for PGIP interfaces *)
   32.51  
   32.52 -val preferences = ref Preferences.pure_preferences;
   32.53 +val preferences = Unsynchronized.ref Preferences.pure_preferences;
   32.54  
   32.55  fun add_preference cat pref =
   32.56 -  CRITICAL (fn () => change preferences (Preferences.add cat pref));
   32.57 +  CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
   32.58  
   32.59  fun setup_preferences_tweak () =
   32.60 -  CRITICAL (fn () => change preferences
   32.61 +  CRITICAL (fn () => Unsynchronized.change preferences
   32.62     (Preferences.set_default ("show-question-marks", "false") #>
   32.63      Preferences.remove "show-question-marks" #>   (* we use markup, not ?s *)
   32.64      Preferences.remove "theorem-dependencies" #>  (* set internally *)
   32.65 @@ -471,7 +471,7 @@
   32.66  fun set_proverflag_pgmlsymbols b =
   32.67      (pgmlsymbols_flag := b;
   32.68        NAMED_CRITICAL "print_mode" (fn () =>
   32.69 -        change print_mode
   32.70 +        Unsynchronized.change print_mode
   32.71              (fn mode =>
   32.72                  remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
   32.73  
   32.74 @@ -677,7 +677,7 @@
   32.75     about this special status, but for now we just keep a local reference.
   32.76  *)
   32.77  
   32.78 -val currently_open_file = ref (NONE : pgipurl option)
   32.79 +val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
   32.80  
   32.81  fun get_currently_open_file () = ! currently_open_file;
   32.82  
   32.83 @@ -779,7 +779,7 @@
   32.84  *)
   32.85  
   32.86  local
   32.87 -    val current_working_dir = ref (NONE : string option)
   32.88 +    val current_working_dir = Unsynchronized.ref (NONE : string option)
   32.89  in
   32.90  fun changecwd_dir newdirpath =
   32.91     let
   32.92 @@ -1021,7 +1021,7 @@
   32.93  
   32.94  (* init *)
   32.95  
   32.96 -val initialized = ref false;
   32.97 +val initialized = Unsynchronized.ref false;
   32.98  
   32.99  fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
  32.100    | init_pgip true =
  32.101 @@ -1035,9 +1035,9 @@
  32.102           setup_present_hook ();
  32.103           init_pgip_session_id ();
  32.104           welcome ();
  32.105 -         set initialized);
  32.106 +         Unsynchronized.set initialized);
  32.107          sync_thy_loader ();
  32.108 -       change print_mode (update (op =) proof_generalN);
  32.109 +       Unsynchronized.change print_mode (update (op =) proof_generalN);
  32.110         pgip_toplevel tty_src);
  32.111  
  32.112  
  32.113 @@ -1045,7 +1045,7 @@
  32.114  (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
  32.115  
  32.116  local
  32.117 -    val pgip_output_channel = ref Output.writeln_default
  32.118 +    val pgip_output_channel = Unsynchronized.ref Output.writeln_default
  32.119  in
  32.120  
  32.121  (* Set recipient for PGIP results *)
    33.1 --- a/src/Pure/ROOT.ML	Tue Sep 29 11:48:32 2009 +0200
    33.2 +++ b/src/Pure/ROOT.ML	Tue Sep 29 11:49:22 2009 +0200
    33.3 @@ -8,7 +8,7 @@
    33.4  end;
    33.5  
    33.6  (*if true then some tools will OMIT some proofs*)
    33.7 -val quick_and_dirty = ref false;
    33.8 +val quick_and_dirty = Unsynchronized.ref false;
    33.9  
   33.10  print_depth 10;
   33.11  
    34.1 --- a/src/Pure/Syntax/ast.ML	Tue Sep 29 11:48:32 2009 +0200
    34.2 +++ b/src/Pure/Syntax/ast.ML	Tue Sep 29 11:49:22 2009 +0200
    34.3 @@ -24,8 +24,8 @@
    34.4    val fold_ast_p: string -> ast list * ast -> ast
    34.5    val unfold_ast: string -> ast -> ast list
    34.6    val unfold_ast_p: string -> ast -> ast list * ast
    34.7 -  val trace_ast: bool ref
    34.8 -  val stat_ast: bool ref
    34.9 +  val trace_ast: bool Unsynchronized.ref
   34.10 +  val stat_ast: bool Unsynchronized.ref
   34.11  end;
   34.12  
   34.13  signature AST =
   34.14 @@ -173,9 +173,9 @@
   34.15  
   34.16  fun normalize trace stat get_rules pre_ast =
   34.17    let
   34.18 -    val passes = ref 0;
   34.19 -    val failed_matches = ref 0;
   34.20 -    val changes = ref 0;
   34.21 +    val passes = Unsynchronized.ref 0;
   34.22 +    val failed_matches = Unsynchronized.ref 0;
   34.23 +    val changes = Unsynchronized.ref 0;
   34.24  
   34.25      fun subst _ (ast as Constant _) = ast
   34.26        | subst env (Variable x) = the (Symtab.lookup env x)
   34.27 @@ -184,8 +184,8 @@
   34.28      fun try_rules ((lhs, rhs) :: pats) ast =
   34.29            (case match ast lhs of
   34.30              SOME (env, args) =>
   34.31 -              (inc changes; SOME (mk_appl (subst env rhs) args))
   34.32 -          | NONE => (inc failed_matches; try_rules pats ast))
   34.33 +              (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args))
   34.34 +          | NONE => (Unsynchronized.inc failed_matches; try_rules pats ast))
   34.35        | try_rules [] _ = NONE;
   34.36      val try_headless_rules = try_rules (get_rules "");
   34.37  
   34.38 @@ -226,7 +226,7 @@
   34.39          val old_changes = ! changes;
   34.40          val new_ast = norm ast;
   34.41        in
   34.42 -        inc passes;
   34.43 +        Unsynchronized.inc passes;
   34.44          if old_changes = ! changes then new_ast else normal new_ast
   34.45        end;
   34.46  
   34.47 @@ -245,8 +245,8 @@
   34.48  
   34.49  (* normalize_ast *)
   34.50  
   34.51 -val trace_ast = ref false;
   34.52 -val stat_ast = ref false;
   34.53 +val trace_ast = Unsynchronized.ref false;
   34.54 +val stat_ast = Unsynchronized.ref false;
   34.55  
   34.56  fun normalize_ast get_rules ast =
   34.57    normalize (! trace_ast) (! stat_ast) get_rules ast;
    35.1 --- a/src/Pure/Syntax/parser.ML	Tue Sep 29 11:48:32 2009 +0200
    35.2 +++ b/src/Pure/Syntax/parser.ML	Tue Sep 29 11:49:22 2009 +0200
    35.3 @@ -17,7 +17,7 @@
    35.4      Tip of Lexicon.token
    35.5    val parse: gram -> string -> Lexicon.token list -> parsetree list
    35.6    val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
    35.7 -  val branching_level: int ref
    35.8 +  val branching_level: int Unsynchronized.ref
    35.9  end;
   35.10  
   35.11  structure Parser: PARSER =
   35.12 @@ -690,7 +690,7 @@
   35.13        else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
   35.14  
   35.15  
   35.16 -val branching_level = ref 600;                   (*trigger value for warnings*)
   35.17 +val branching_level = Unsynchronized.ref 600;   (*trigger value for warnings*)
   35.18  
   35.19  (*get all productions of a NT and NTs chained to it which can
   35.20    be started by specified token*)
   35.21 @@ -821,7 +821,7 @@
   35.22      val Estate = Array.array (s, []);
   35.23    in
   35.24      Array.update (Estate, 0, S0);
   35.25 -    get_trees (produce (ref false) prods tags chains Estate 0 indata eof)
   35.26 +    get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata eof)
   35.27    end;
   35.28  
   35.29  
    36.1 --- a/src/Pure/Syntax/printer.ML	Tue Sep 29 11:48:32 2009 +0200
    36.2 +++ b/src/Pure/Syntax/printer.ML	Tue Sep 29 11:49:22 2009 +0200
    36.3 @@ -6,11 +6,11 @@
    36.4  
    36.5  signature PRINTER0 =
    36.6  sig
    36.7 -  val show_brackets: bool ref
    36.8 -  val show_sorts: bool ref
    36.9 -  val show_types: bool ref
   36.10 -  val show_no_free_types: bool ref
   36.11 -  val show_all_types: bool ref
   36.12 +  val show_brackets: bool Unsynchronized.ref
   36.13 +  val show_sorts: bool Unsynchronized.ref
   36.14 +  val show_types: bool Unsynchronized.ref
   36.15 +  val show_no_free_types: bool Unsynchronized.ref
   36.16 +  val show_all_types: bool Unsynchronized.ref
   36.17    val pp_show_brackets: Pretty.pp -> Pretty.pp
   36.18  end;
   36.19  
   36.20 @@ -42,11 +42,11 @@
   36.21  
   36.22  (** options for printing **)
   36.23  
   36.24 -val show_types = ref false;
   36.25 -val show_sorts = ref false;
   36.26 -val show_brackets = ref false;
   36.27 -val show_no_free_types = ref false;
   36.28 -val show_all_types = ref false;
   36.29 +val show_types = Unsynchronized.ref false;
   36.30 +val show_sorts = Unsynchronized.ref false;
   36.31 +val show_brackets = Unsynchronized.ref false;
   36.32 +val show_no_free_types = Unsynchronized.ref false;
   36.33 +val show_all_types = Unsynchronized.ref false;
   36.34  
   36.35  fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp),
   36.36    Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
    37.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Sep 29 11:48:32 2009 +0200
    37.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Sep 29 11:49:22 2009 +0200
    37.3 @@ -6,7 +6,7 @@
    37.4  
    37.5  signature SYN_TRANS0 =
    37.6  sig
    37.7 -  val eta_contract: bool ref
    37.8 +  val eta_contract: bool Unsynchronized.ref
    37.9    val atomic_abs_tr': string * typ * term -> term * term
   37.10    val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
   37.11    val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
   37.12 @@ -276,7 +276,7 @@
   37.13  
   37.14  (*do (partial) eta-contraction before printing*)
   37.15  
   37.16 -val eta_contract = ref true;
   37.17 +val eta_contract = Unsynchronized.ref true;
   37.18  
   37.19  fun eta_contr tm =
   37.20    let
    38.1 --- a/src/Pure/Syntax/syntax.ML	Tue Sep 29 11:48:32 2009 +0200
    38.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Sep 29 11:49:22 2009 +0200
    38.3 @@ -36,9 +36,9 @@
    38.4    val print_syntax: syntax -> unit
    38.5    val guess_infix: syntax -> string -> mixfix option
    38.6    val read_token: string -> Symbol_Pos.T list * Position.T
    38.7 -  val ambiguity_is_error: bool ref
    38.8 -  val ambiguity_level: int ref
    38.9 -  val ambiguity_limit: int ref
   38.10 +  val ambiguity_is_error: bool Unsynchronized.ref
   38.11 +  val ambiguity_level: int Unsynchronized.ref
   38.12 +  val ambiguity_limit: int Unsynchronized.ref
   38.13    val standard_parse_term: Pretty.pp -> (term -> string option) ->
   38.14      (((string * int) * sort) list -> string * int -> Term.sort) ->
   38.15      (string -> bool * string) -> (string -> string option) ->
   38.16 @@ -472,9 +472,9 @@
   38.17  
   38.18  (* read_ast *)
   38.19  
   38.20 -val ambiguity_is_error = ref false;
   38.21 -val ambiguity_level = ref 1;
   38.22 -val ambiguity_limit = ref 10;
   38.23 +val ambiguity_is_error = Unsynchronized.ref false;
   38.24 +val ambiguity_level = Unsynchronized.ref 1;
   38.25 +val ambiguity_limit = Unsynchronized.ref 10;
   38.26  
   38.27  fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
   38.28  
   38.29 @@ -711,7 +711,7 @@
   38.30      unparse_typ: Proof.context -> typ -> Pretty.T,
   38.31      unparse_term: Proof.context -> term -> Pretty.T};
   38.32  
   38.33 -  val operations = ref (NONE: operations option);
   38.34 +  val operations = Unsynchronized.ref (NONE: operations option);
   38.35  
   38.36    fun operation which ctxt x =
   38.37      (case ! operations of
    39.1 --- a/src/Pure/System/isabelle_process.ML	Tue Sep 29 11:48:32 2009 +0200
    39.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Sep 29 11:49:22 2009 +0200
    39.3 @@ -130,7 +130,7 @@
    39.4  (* init *)
    39.5  
    39.6  fun init out =
    39.7 - (change print_mode (update (op =) isabelle_processN);
    39.8 + (Unsynchronized.change print_mode (update (op =) isabelle_processN);
    39.9    setup_channels out |> init_message;
   39.10    OuterKeyword.report ();
   39.11    Output.status (Markup.markup Markup.ready "");
    40.1 --- a/src/Pure/System/isar.ML	Tue Sep 29 11:48:32 2009 +0200
    40.2 +++ b/src/Pure/System/isar.ML	Tue Sep 29 11:49:22 2009 +0200
    40.3 @@ -18,7 +18,7 @@
    40.4    val undo: int -> unit
    40.5    val kill: unit -> unit
    40.6    val kill_proof: unit -> unit
    40.7 -  val crashes: exn list ref
    40.8 +  val crashes: exn list Unsynchronized.ref
    40.9    val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   40.10    val loop: unit -> unit
   40.11    val main: unit -> unit
   40.12 @@ -36,9 +36,9 @@
   40.13    (*previous state, state transition -- regular commands only*)
   40.14  
   40.15  local
   40.16 -  val global_history = ref ([]: history);
   40.17 -  val global_state = ref Toplevel.toplevel;
   40.18 -  val global_exn = ref (NONE: (exn * string) option);
   40.19 +  val global_history = Unsynchronized.ref ([]: history);
   40.20 +  val global_state = Unsynchronized.ref Toplevel.toplevel;
   40.21 +  val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
   40.22  in
   40.23  
   40.24  fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
   40.25 @@ -115,7 +115,7 @@
   40.26  
   40.27  (* toplevel loop *)
   40.28  
   40.29 -val crashes = ref ([]: exn list);
   40.30 +val crashes = Unsynchronized.ref ([]: exn list);
   40.31  
   40.32  local
   40.33  
   40.34 @@ -130,7 +130,7 @@
   40.35      handle exn =>
   40.36        (Output.error_msg (ML_Compiler.exn_message exn)
   40.37          handle crash =>
   40.38 -          (CRITICAL (fn () => change crashes (cons crash));
   40.39 +          (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
   40.40              warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
   40.41            raw_loop secure src)
   40.42    end;
    41.1 --- a/src/Pure/System/session.ML	Tue Sep 29 11:48:32 2009 +0200
    41.2 +++ b/src/Pure/System/session.ML	Tue Sep 29 11:49:22 2009 +0200
    41.3 @@ -21,10 +21,10 @@
    41.4  
    41.5  (* session state *)
    41.6  
    41.7 -val session = ref ([Context.PureN]: string list);
    41.8 -val session_path = ref ([]: string list);
    41.9 -val session_finished = ref false;
   41.10 -val remote_path = ref (NONE: Url.T option);
   41.11 +val session = Unsynchronized.ref ([Context.PureN]: string list);
   41.12 +val session_path = Unsynchronized.ref ([]: string list);
   41.13 +val session_finished = Unsynchronized.ref false;
   41.14 +val remote_path = Unsynchronized.ref (NONE: Url.T option);
   41.15  
   41.16  
   41.17  (* access path *)
    42.1 --- a/src/Pure/Thy/html.ML	Tue Sep 29 11:48:32 2009 +0200
    42.2 +++ b/src/Pure/Thy/html.ML	Tue Sep 29 11:49:22 2009 +0200
    42.3 @@ -267,8 +267,8 @@
    42.4  
    42.5  (* document *)
    42.6  
    42.7 -val charset = ref "ISO-8859-1";
    42.8 -fun with_charset s = setmp_noncritical charset s;
    42.9 +val charset = Unsynchronized.ref "ISO-8859-1";
   42.10 +fun with_charset s = setmp_noncritical charset s;   (* FIXME *)
   42.11  
   42.12  fun begin_document title =
   42.13    let val cs = ! charset in
    43.1 --- a/src/Pure/Thy/present.ML	Tue Sep 29 11:48:32 2009 +0200
    43.2 +++ b/src/Pure/Thy/present.ML	Tue Sep 29 11:49:22 2009 +0200
    43.3 @@ -161,10 +161,11 @@
    43.4  
    43.5  (* state *)
    43.6  
    43.7 -val browser_info = ref empty_browser_info;
    43.8 -fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
    43.9 +val browser_info = Unsynchronized.ref empty_browser_info;
   43.10 +fun change_browser_info f =
   43.11 +  CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
   43.12  
   43.13 -val suppress_tex_source = ref false;
   43.14 +val suppress_tex_source = Unsynchronized.ref false;
   43.15  fun no_document f x = setmp_noncritical suppress_tex_source true f x;
   43.16  
   43.17  fun init_theory_info name info =
   43.18 @@ -229,7 +230,7 @@
   43.19  
   43.20  (* state *)
   43.21  
   43.22 -val session_info = ref (NONE: session_info option);
   43.23 +val session_info = Unsynchronized.ref (NONE: session_info option);
   43.24  
   43.25  fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
   43.26  fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
   43.27 @@ -534,5 +535,5 @@
   43.28  
   43.29  end;
   43.30  
   43.31 -structure BasicPresent: BASIC_PRESENT = Present;
   43.32 -open BasicPresent;
   43.33 +structure Basic_Present: BASIC_PRESENT = Present;
   43.34 +open Basic_Present;
    44.1 --- a/src/Pure/Thy/thy_info.ML	Tue Sep 29 11:48:32 2009 +0200
    44.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Sep 29 11:49:22 2009 +0200
    44.3 @@ -50,9 +50,9 @@
    44.4  val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
    44.5  
    44.6  local
    44.7 -  val hooks = ref ([]: (action -> string -> unit) list);
    44.8 +  val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
    44.9  in
   44.10 -  fun add_hook f = CRITICAL (fn () => change hooks (cons f));
   44.11 +  fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
   44.12    fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
   44.13  end;
   44.14  
   44.15 @@ -111,10 +111,10 @@
   44.16  type thy = deps option * theory option;
   44.17  
   44.18  local
   44.19 -  val database = ref (Graph.empty: thy Graph.T);
   44.20 +  val database = Unsynchronized.ref (Graph.empty: thy Graph.T);
   44.21  in
   44.22    fun get_thys () = ! database;
   44.23 -  fun change_thys f = CRITICAL (fn () => Library.change database f);
   44.24 +  fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
   44.25  end;
   44.26  
   44.27  
    45.1 --- a/src/Pure/Thy/thy_load.ML	Tue Sep 29 11:48:32 2009 +0200
    45.2 +++ b/src/Pure/Thy/thy_load.ML	Tue Sep 29 11:49:22 2009 +0200
    45.3 @@ -37,14 +37,16 @@
    45.4  
    45.5  (* maintain load path *)
    45.6  
    45.7 -local val load_path = ref [Path.current] in
    45.8 +local val load_path = Unsynchronized.ref [Path.current] in
    45.9  
   45.10  fun show_path () = map Path.implode (! load_path);
   45.11  
   45.12 -fun del_path s = CRITICAL (fn () => change load_path (remove (op =) (Path.explode s)));
   45.13 -fun add_path s = CRITICAL (fn () => (del_path s; change load_path (cons (Path.explode s))));
   45.14 -fun path_add s =
   45.15 -  CRITICAL (fn () => (del_path s; change load_path (fn path => path @ [Path.explode s])));
   45.16 +fun del_path s = CRITICAL (fn () =>
   45.17 +    Unsynchronized.change load_path (remove (op =) (Path.explode s)));
   45.18 +fun add_path s = CRITICAL (fn () =>
   45.19 +    (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
   45.20 +fun path_add s = CRITICAL (fn () =>
   45.21 +    (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
   45.22  fun reset_path () = load_path := [Path.current];
   45.23  
   45.24  fun with_paths ss f x =
   45.25 @@ -124,5 +126,5 @@
   45.26  
   45.27  end;
   45.28  
   45.29 -structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
   45.30 -open BasicThyLoad;
   45.31 +structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
   45.32 +open Basic_Thy_Load;
    46.1 --- a/src/Pure/Thy/thy_output.ML	Tue Sep 29 11:48:32 2009 +0200
    46.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Sep 29 11:49:22 2009 +0200
    46.3 @@ -6,11 +6,11 @@
    46.4  
    46.5  signature THY_OUTPUT =
    46.6  sig
    46.7 -  val display: bool ref
    46.8 -  val quotes: bool ref
    46.9 -  val indent: int ref
   46.10 -  val source: bool ref
   46.11 -  val break: bool ref
   46.12 +  val display: bool Unsynchronized.ref
   46.13 +  val quotes: bool Unsynchronized.ref
   46.14 +  val indent: int Unsynchronized.ref
   46.15 +  val source: bool Unsynchronized.ref
   46.16 +  val break: bool Unsynchronized.ref
   46.17    val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
   46.18    val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
   46.19    val defined_command: string -> bool
   46.20 @@ -21,7 +21,7 @@
   46.21    val antiquotation: string -> 'a context_parser ->
   46.22      ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
   46.23    datatype markup = Markup | MarkupEnv | Verbatim
   46.24 -  val modes: string list ref
   46.25 +  val modes: string list Unsynchronized.ref
   46.26    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   46.27    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
   46.28      (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
   46.29 @@ -42,11 +42,11 @@
   46.30  
   46.31  (** global options **)
   46.32  
   46.33 -val display = ref false;
   46.34 -val quotes = ref false;
   46.35 -val indent = ref 0;
   46.36 -val source = ref false;
   46.37 -val break = ref false;
   46.38 +val display = Unsynchronized.ref false;
   46.39 +val quotes = Unsynchronized.ref false;
   46.40 +val indent = Unsynchronized.ref 0;
   46.41 +val source = Unsynchronized.ref false;
   46.42 +val break = Unsynchronized.ref false;
   46.43  
   46.44  
   46.45  
   46.46 @@ -55,10 +55,10 @@
   46.47  local
   46.48  
   46.49  val global_commands =
   46.50 -  ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
   46.51 +  Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
   46.52  
   46.53  val global_options =
   46.54 -  ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
   46.55 +  Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
   46.56  
   46.57  fun add_item kind (name, x) tab =
   46.58   (if not (Symtab.defined tab name) then ()
   46.59 @@ -67,8 +67,10 @@
   46.60  
   46.61  in
   46.62  
   46.63 -fun add_commands xs = CRITICAL (fn () => change global_commands (fold (add_item "command") xs));
   46.64 -fun add_options xs = CRITICAL (fn () => change global_options (fold (add_item "option") xs));
   46.65 +fun add_commands xs =
   46.66 +  CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs));
   46.67 +fun add_options xs =
   46.68 +  CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs));
   46.69  
   46.70  fun defined_command name = Symtab.defined (! global_commands) name;
   46.71  fun defined_option name = Symtab.defined (! global_options) name;
   46.72 @@ -143,7 +145,7 @@
   46.73  
   46.74  (* eval_antiquote *)
   46.75  
   46.76 -val modes = ref ([]: string list);
   46.77 +val modes = Unsynchronized.ref ([]: string list);
   46.78  
   46.79  fun eval_antiquote lex state (txt, pos) =
   46.80    let
    47.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Sep 29 11:48:32 2009 +0200
    47.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Sep 29 11:49:22 2009 +0200
    47.3 @@ -9,8 +9,8 @@
    47.4    datatype 'term criterion =
    47.5      Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
    47.6      Pattern of 'term
    47.7 -  val tac_limit: int ref
    47.8 -  val limit: int ref
    47.9 +  val tac_limit: int Unsynchronized.ref
   47.10 +  val limit: int Unsynchronized.ref
   47.11    val find_theorems: Proof.context -> thm option -> int option -> bool ->
   47.12      (bool * string criterion) list -> int option * (Facts.ref * thm) list
   47.13    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
   47.14 @@ -186,7 +186,7 @@
   47.15      end
   47.16    else NONE
   47.17  
   47.18 -val tac_limit = ref 5;
   47.19 +val tac_limit = Unsynchronized.ref 5;
   47.20  
   47.21  fun filter_solves ctxt goal =
   47.22    let
   47.23 @@ -372,7 +372,7 @@
   47.24     (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @
   47.25      Facts.dest_static [] (ProofContext.facts_of ctxt));
   47.26  
   47.27 -val limit = ref 40;
   47.28 +val limit = Unsynchronized.ref 40;
   47.29  
   47.30  fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   47.31    let
    48.1 --- a/src/Pure/codegen.ML	Tue Sep 29 11:48:32 2009 +0200
    48.2 +++ b/src/Pure/codegen.ML	Tue Sep 29 11:49:22 2009 +0200
    48.3 @@ -6,10 +6,10 @@
    48.4  
    48.5  signature CODEGEN =
    48.6  sig
    48.7 -  val quiet_mode : bool ref
    48.8 +  val quiet_mode : bool Unsynchronized.ref
    48.9    val message : string -> unit
   48.10 -  val mode : string list ref
   48.11 -  val margin : int ref
   48.12 +  val mode : string list Unsynchronized.ref
   48.13 +  val margin : int Unsynchronized.ref
   48.14    val string_of : Pretty.T -> string
   48.15    val str : string -> Pretty.T
   48.16  
   48.17 @@ -75,9 +75,9 @@
   48.18    val mk_type: bool -> typ -> Pretty.T
   48.19    val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
   48.20    val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
   48.21 -  val test_fn: (int -> term list option) ref
   48.22 +  val test_fn: (int -> term list option) Unsynchronized.ref
   48.23    val test_term: Proof.context -> term -> int -> term list option
   48.24 -  val eval_result: (unit -> term) ref
   48.25 +  val eval_result: (unit -> term) Unsynchronized.ref
   48.26    val eval_term: theory -> term -> term
   48.27    val evaluation_conv: cterm -> thm
   48.28    val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
   48.29 @@ -102,12 +102,12 @@
   48.30  structure Codegen : CODEGEN =
   48.31  struct
   48.32  
   48.33 -val quiet_mode = ref true;
   48.34 +val quiet_mode = Unsynchronized.ref true;
   48.35  fun message s = if !quiet_mode then () else writeln s;
   48.36  
   48.37 -val mode = ref ([] : string list);
   48.38 +val mode = Unsynchronized.ref ([] : string list);
   48.39  
   48.40 -val margin = ref 80;
   48.41 +val margin = Unsynchronized.ref 80;
   48.42  
   48.43  fun string_of p = (Pretty.string_of |>
   48.44    PrintMode.setmp [] |>
   48.45 @@ -878,7 +878,8 @@
   48.46                [mk_gen gr module true xs a T, mk_type true T]) Ts) @
   48.47           (if member (op =) xs s then [str a] else []))));
   48.48  
   48.49 -val test_fn : (int -> term list option) ref = ref (fn _ => NONE);
   48.50 +val test_fn : (int -> term list option) Unsynchronized.ref =
   48.51 +  Unsynchronized.ref (fn _ => NONE);
   48.52  
   48.53  fun test_term ctxt t =
   48.54    let
   48.55 @@ -912,7 +913,7 @@
   48.56  
   48.57  (**** Evaluator for terms ****)
   48.58  
   48.59 -val eval_result = ref (fn () => Bound 0);
   48.60 +val eval_result = Unsynchronized.ref (fn () => Bound 0);
   48.61  
   48.62  fun eval_term thy t =
   48.63    let
    49.1 --- a/src/Pure/context.ML	Tue Sep 29 11:48:32 2009 +0200
    49.2 +++ b/src/Pure/context.ML	Tue Sep 29 11:49:22 2009 +0200
    49.3 @@ -107,7 +107,7 @@
    49.4    extend: Object.T -> Object.T,
    49.5    merge: Pretty.pp -> Object.T * Object.T -> Object.T};
    49.6  
    49.7 -val kinds = ref (Datatab.empty: kind Datatab.table);
    49.8 +val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
    49.9  
   49.10  fun invoke f k =
   49.11    (case Datatab.lookup (! kinds) k of
   49.12 @@ -125,7 +125,7 @@
   49.13    let
   49.14      val k = serial ();
   49.15      val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
   49.16 -    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
   49.17 +    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
   49.18    in k end;
   49.19  
   49.20  val copy_data = Datatab.map' invoke_copy;
   49.21 @@ -149,7 +149,7 @@
   49.22  datatype theory =
   49.23    Theory of
   49.24     (*identity*)
   49.25 -   {self: theory ref option,      (*dynamic self reference -- follows theory changes*)
   49.26 +   {self: theory Unsynchronized.ref option,  (*dynamic self reference -- follows theory changes*)
   49.27      draft: bool,                  (*draft mode -- linear destructive changes*)
   49.28      id: serial,                   (*identifier*)
   49.29      ids: unit Inttab.table} *     (*cumulative identifiers of non-drafts -- symbolic body content*)
   49.30 @@ -186,14 +186,15 @@
   49.31  fun eq_id (i: int, j) = i = j;
   49.32  
   49.33  fun is_stale
   49.34 -    (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
   49.35 +    (Theory ({self =
   49.36 +        SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
   49.37        not (eq_id (id, id'))
   49.38    | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
   49.39  
   49.40  fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
   49.41    | vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
   49.42        let
   49.43 -        val r = ref thy;
   49.44 +        val r = Unsynchronized.ref thy;
   49.45          val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
   49.46        in r := thy'; thy' end;
   49.47  
   49.48 @@ -243,9 +244,9 @@
   49.49    theory in external data structures -- a plain theory value would
   49.50    become stale as the self reference moves on*)
   49.51  
   49.52 -datatype theory_ref = TheoryRef of theory ref;
   49.53 +datatype theory_ref = TheoryRef of theory Unsynchronized.ref;
   49.54  
   49.55 -fun deref (TheoryRef (ref thy)) = thy;
   49.56 +fun deref (TheoryRef (Unsynchronized.ref thy)) = thy;
   49.57  
   49.58  fun check_thy thy =  (*thread-safe version*)
   49.59    let val thy_ref = TheoryRef (the_self thy) in
   49.60 @@ -437,7 +438,7 @@
   49.61  
   49.62  local
   49.63  
   49.64 -val kinds = ref (Datatab.empty: (theory -> Object.T) Datatab.table);
   49.65 +val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
   49.66  
   49.67  fun invoke_init k =
   49.68    (case Datatab.lookup (! kinds) k of
   49.69 @@ -470,7 +471,7 @@
   49.70  fun declare init =
   49.71    let
   49.72      val k = serial ();
   49.73 -    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
   49.74 +    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
   49.75    in k end;
   49.76  
   49.77  fun get k dest prf =
    50.1 --- a/src/Pure/display.ML	Tue Sep 29 11:48:32 2009 +0200
    50.2 +++ b/src/Pure/display.ML	Tue Sep 29 11:49:22 2009 +0200
    50.3 @@ -7,10 +7,10 @@
    50.4  
    50.5  signature BASIC_DISPLAY =
    50.6  sig
    50.7 -  val goals_limit: int ref
    50.8 -  val show_consts: bool ref
    50.9 -  val show_hyps: bool ref
   50.10 -  val show_tags: bool ref
   50.11 +  val goals_limit: int Unsynchronized.ref
   50.12 +  val show_consts: bool Unsynchronized.ref
   50.13 +  val show_hyps: bool Unsynchronized.ref
   50.14 +  val show_tags: bool Unsynchronized.ref
   50.15  end;
   50.16  
   50.17  signature DISPLAY =
   50.18 @@ -39,8 +39,8 @@
   50.19  val goals_limit = Goal_Display.goals_limit;
   50.20  val show_consts = Goal_Display.show_consts;
   50.21  
   50.22 -val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
   50.23 -val show_tags = ref false;      (*false: suppress tags*)
   50.24 +val show_hyps = Unsynchronized.ref false;    (*false: print meta-hypotheses as dots*)
   50.25 +val show_tags = Unsynchronized.ref false;    (*false: suppress tags*)
   50.26  
   50.27  
   50.28  
    51.1 --- a/src/Pure/goal.ML	Tue Sep 29 11:48:32 2009 +0200
    51.2 +++ b/src/Pure/goal.ML	Tue Sep 29 11:49:22 2009 +0200
    51.3 @@ -6,7 +6,7 @@
    51.4  
    51.5  signature BASIC_GOAL =
    51.6  sig
    51.7 -  val parallel_proofs: int ref
    51.8 +  val parallel_proofs: int Unsynchronized.ref
    51.9    val SELECT_GOAL: tactic -> int -> tactic
   51.10    val CONJUNCTS: tactic -> int -> tactic
   51.11    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
   51.12 @@ -102,7 +102,7 @@
   51.13  
   51.14  (* future_enabled *)
   51.15  
   51.16 -val parallel_proofs = ref 1;
   51.17 +val parallel_proofs = Unsynchronized.ref 1;
   51.18  
   51.19  fun future_enabled () =
   51.20    Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
    52.1 --- a/src/Pure/goal_display.ML	Tue Sep 29 11:48:32 2009 +0200
    52.2 +++ b/src/Pure/goal_display.ML	Tue Sep 29 11:49:22 2009 +0200
    52.3 @@ -7,8 +7,8 @@
    52.4  
    52.5  signature GOAL_DISPLAY =
    52.6  sig
    52.7 -  val goals_limit: int ref
    52.8 -  val show_consts: bool ref
    52.9 +  val goals_limit: int Unsynchronized.ref
   52.10 +  val show_consts: bool Unsynchronized.ref
   52.11    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   52.12    val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
   52.13      thm -> Pretty.T list
   52.14 @@ -18,8 +18,8 @@
   52.15  structure Goal_Display: GOAL_DISPLAY =
   52.16  struct
   52.17  
   52.18 -val goals_limit = ref 10;      (*max number of goals to print*)
   52.19 -val show_consts = ref false;   (*true: show consts with types in proof state output*)
   52.20 +val goals_limit = Unsynchronized.ref 10;     (*max number of goals to print*)
   52.21 +val show_consts = Unsynchronized.ref false;  (*true: show consts with types in proof state output*)
   52.22  
   52.23  fun pretty_flexpair ctxt (t, u) = Pretty.block
   52.24    [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    53.1 --- a/src/Pure/meta_simplifier.ML	Tue Sep 29 11:48:32 2009 +0200
    53.2 +++ b/src/Pure/meta_simplifier.ML	Tue Sep 29 11:49:22 2009 +0200
    53.3 @@ -11,9 +11,9 @@
    53.4  
    53.5  signature BASIC_META_SIMPLIFIER =
    53.6  sig
    53.7 -  val debug_simp: bool ref
    53.8 -  val trace_simp: bool ref
    53.9 -  val trace_simp_depth_limit: int ref
   53.10 +  val debug_simp: bool Unsynchronized.ref
   53.11 +  val trace_simp: bool Unsynchronized.ref
   53.12 +  val trace_simp_depth_limit: int Unsynchronized.ref
   53.13    type rrule
   53.14    val eq_rrule: rrule * rrule -> bool
   53.15    type simpset
   53.16 @@ -84,7 +84,7 @@
   53.17     {rules: rrule Net.net,
   53.18      prems: thm list,
   53.19      bounds: int * ((string * typ) * string) list,
   53.20 -    depth: int * bool ref,
   53.21 +    depth: int * bool Unsynchronized.ref,
   53.22      context: Proof.context option} *
   53.23     {congs: (string * thm) list * string list,
   53.24      procs: proc Net.net,
   53.25 @@ -112,7 +112,7 @@
   53.26    val the_context: simpset -> Proof.context
   53.27    val context: Proof.context -> simpset -> simpset
   53.28    val theory_context: theory  -> simpset -> simpset
   53.29 -  val debug_bounds: bool ref
   53.30 +  val debug_bounds: bool Unsynchronized.ref
   53.31    val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
   53.32    val set_solvers: solver list -> simpset -> simpset
   53.33    val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
   53.34 @@ -190,7 +190,7 @@
   53.35     {rules: rrule Net.net,
   53.36      prems: thm list,
   53.37      bounds: int * ((string * typ) * string) list,
   53.38 -    depth: int * bool ref,
   53.39 +    depth: int * bool Unsynchronized.ref,
   53.40      context: Proof.context option} *
   53.41     {congs: (string * thm) list * string list,
   53.42      procs: proc Net.net,
   53.43 @@ -256,7 +256,7 @@
   53.44  val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
   53.45  val simp_depth_limit = Config.int simp_depth_limit_value;
   53.46  
   53.47 -val trace_simp_depth_limit = ref 1;
   53.48 +val trace_simp_depth_limit = Unsynchronized.ref 1;
   53.49  
   53.50  fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
   53.51    if depth > ! trace_simp_depth_limit then
   53.52 @@ -266,7 +266,8 @@
   53.53  
   53.54  val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
   53.55    (rules, prems, bounds,
   53.56 -    (depth + 1, if depth = ! trace_simp_depth_limit then ref false else exceeded), context));
   53.57 +    (depth + 1,
   53.58 +      if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
   53.59  
   53.60  fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
   53.61  
   53.62 @@ -275,8 +276,8 @@
   53.63  
   53.64  exception SIMPLIFIER of string * thm;
   53.65  
   53.66 -val debug_simp = ref false;
   53.67 -val trace_simp = ref false;
   53.68 +val debug_simp = Unsynchronized.ref false;
   53.69 +val trace_simp = Unsynchronized.ref false;
   53.70  
   53.71  local
   53.72  
   53.73 @@ -746,7 +747,7 @@
   53.74  (* empty *)
   53.75  
   53.76  fun init_ss mk_rews termless subgoal_tac solvers =
   53.77 -  make_simpset ((Net.empty, [], (0, []), (0, ref false), NONE),
   53.78 +  make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
   53.79      (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
   53.80  
   53.81  fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
   53.82 @@ -1209,7 +1210,7 @@
   53.83      prover: how to solve premises in conditional rewrites and congruences
   53.84  *)
   53.85  
   53.86 -val debug_bounds = ref false;
   53.87 +val debug_bounds = Unsynchronized.ref false;
   53.88  
   53.89  fun check_bounds ss ct =
   53.90    if ! debug_bounds then
   53.91 @@ -1337,5 +1338,5 @@
   53.92  
   53.93  end;
   53.94  
   53.95 -structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
   53.96 -open BasicMetaSimplifier;
   53.97 +structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
   53.98 +open Basic_Meta_Simplifier;
    54.1 --- a/src/Pure/old_goals.ML	Tue Sep 29 11:48:32 2009 +0200
    54.2 +++ b/src/Pure/old_goals.ML	Tue Sep 29 11:49:22 2009 +0200
    54.3 @@ -19,7 +19,7 @@
    54.4    type proof
    54.5    val premises: unit -> thm list
    54.6    val reset_goals: unit -> unit
    54.7 -  val result_error_fn: (thm -> string -> thm) ref
    54.8 +  val result_error_fn: (thm -> string -> thm) Unsynchronized.ref
    54.9    val print_sign_exn: theory -> exn -> 'a
   54.10    val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
   54.11    val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
   54.12 @@ -233,21 +233,21 @@
   54.13  (*** References ***)
   54.14  
   54.15  (*Current assumption list -- set by "goal".*)
   54.16 -val curr_prems = ref([] : thm list);
   54.17 +val curr_prems = Unsynchronized.ref([] : thm list);
   54.18  
   54.19  (*Return assumption list -- useful if you didn't save "goal"'s result. *)
   54.20  fun premises() = !curr_prems;
   54.21  
   54.22  (*Current result maker -- set by "goal", used by "result".  *)
   54.23  fun init_mkresult _ = error "No goal has been supplied in subgoal module";
   54.24 -val curr_mkresult = ref (init_mkresult: bool*thm->thm);
   54.25 +val curr_mkresult = Unsynchronized.ref (init_mkresult: bool*thm->thm);
   54.26  
   54.27  (*List of previous goal stacks, for the undo operation.  Set by setstate.
   54.28    A list of lists!*)
   54.29 -val undo_list = ref([[(asm_rl, Seq.empty)]] : gstack list);
   54.30 +val undo_list = Unsynchronized.ref([[(asm_rl, Seq.empty)]] : gstack list);
   54.31  
   54.32  (* Stack of proof attempts *)
   54.33 -val proofstack = ref([]: proof list);
   54.34 +val proofstack = Unsynchronized.ref([]: proof list);
   54.35  
   54.36  (*reset all refs*)
   54.37  fun reset_goals () =
   54.38 @@ -272,7 +272,7 @@
   54.39        Goal_Display.pretty_goals_without_context (!goals_limit) state @
   54.40      [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
   54.41  
   54.42 -val result_error_fn = ref result_error_default;
   54.43 +val result_error_fn = Unsynchronized.ref result_error_default;
   54.44  
   54.45  
   54.46  (*Common treatment of "goal" and "prove_goal":
    55.1 --- a/src/Pure/pattern.ML	Tue Sep 29 11:48:32 2009 +0200
    55.2 +++ b/src/Pure/pattern.ML	Tue Sep 29 11:49:22 2009 +0200
    55.3 @@ -14,7 +14,7 @@
    55.4  
    55.5  signature PATTERN =
    55.6  sig
    55.7 -  val trace_unify_fail: bool ref
    55.8 +  val trace_unify_fail: bool Unsynchronized.ref
    55.9    val aeconv: term * term -> bool
   55.10    val eta_long: typ list -> term -> term
   55.11    val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   55.12 @@ -40,7 +40,7 @@
   55.13  exception Unif;
   55.14  exception Pattern;
   55.15  
   55.16 -val trace_unify_fail = ref false;
   55.17 +val trace_unify_fail = Unsynchronized.ref false;
   55.18  
   55.19  fun string_of_term thy env binders t =
   55.20    Syntax.string_of_term_global thy
    56.1 --- a/src/Pure/proofterm.ML	Tue Sep 29 11:48:32 2009 +0200
    56.2 +++ b/src/Pure/proofterm.ML	Tue Sep 29 11:49:22 2009 +0200
    56.3 @@ -8,7 +8,7 @@
    56.4  
    56.5  signature BASIC_PROOFTERM =
    56.6  sig
    56.7 -  val proofs: int ref
    56.8 +  val proofs: int Unsynchronized.ref
    56.9  
   56.10    datatype proof =
   56.11       MinProof
   56.12 @@ -885,7 +885,7 @@
   56.13  
   56.14  (***** axioms and theorems *****)
   56.15  
   56.16 -val proofs = ref 2;
   56.17 +val proofs = Unsynchronized.ref 2;
   56.18  
   56.19  fun vars_of t = map Var (rev (Term.add_vars t []));
   56.20  fun frees_of t = map Free (rev (Term.add_frees t []));
    57.1 --- a/src/Pure/search.ML	Tue Sep 29 11:48:32 2009 +0200
    57.2 +++ b/src/Pure/search.ML	Tue Sep 29 11:49:22 2009 +0200
    57.3 @@ -13,23 +13,23 @@
    57.4    val THEN_MAYBE        : tactic * tactic -> tactic
    57.5    val THEN_MAYBE'       : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
    57.6  
    57.7 -  val trace_DEPTH_FIRST : bool ref
    57.8 +  val trace_DEPTH_FIRST : bool Unsynchronized.ref
    57.9    val DEPTH_FIRST       : (thm -> bool) -> tactic -> tactic
   57.10    val DEPTH_SOLVE       : tactic -> tactic
   57.11    val DEPTH_SOLVE_1     : tactic -> tactic
   57.12    val ITER_DEEPEN       : (thm->bool) -> (int->tactic) -> tactic
   57.13    val THEN_ITER_DEEPEN  : tactic -> (thm->bool) -> (int->tactic) -> tactic
   57.14 -  val iter_deepen_limit : int ref
   57.15 +  val iter_deepen_limit : int Unsynchronized.ref
   57.16  
   57.17    val has_fewer_prems   : int -> thm -> bool
   57.18    val IF_UNSOLVED       : tactic -> tactic
   57.19    val SOLVE             : tactic -> tactic
   57.20    val DETERM_UNTIL_SOLVED: tactic -> tactic
   57.21 -  val trace_BEST_FIRST  : bool ref
   57.22 +  val trace_BEST_FIRST  : bool Unsynchronized.ref
   57.23    val BEST_FIRST        : (thm -> bool) * (thm -> int) -> tactic -> tactic
   57.24    val THEN_BEST_FIRST   : tactic -> (thm->bool) * (thm->int) -> tactic
   57.25                            -> tactic
   57.26 -  val trace_ASTAR       : bool ref
   57.27 +  val trace_ASTAR       : bool Unsynchronized.ref
   57.28    val ASTAR             : (thm -> bool) * (int->thm->int) -> tactic -> tactic
   57.29    val THEN_ASTAR        : tactic -> (thm->bool) * (int->thm->int) -> tactic
   57.30                            -> tactic
   57.31 @@ -50,7 +50,7 @@
   57.32  
   57.33  (**** Depth-first search ****)
   57.34  
   57.35 -val trace_DEPTH_FIRST = ref false;
   57.36 +val trace_DEPTH_FIRST = Unsynchronized.ref false;
   57.37  
   57.38  (*Searches until "satp" reports proof tree as satisfied.
   57.39    Suppresses duplicate solutions to minimize search space.*)
   57.40 @@ -130,7 +130,7 @@
   57.41  
   57.42  
   57.43  (*No known example (on 1-5-2007) needs even thirty*)
   57.44 -val iter_deepen_limit = ref 50;
   57.45 +val iter_deepen_limit = Unsynchronized.ref 50;
   57.46  
   57.47  (*Depth-first iterative deepening search for a state that satisfies satp
   57.48    tactic tac0 sets up the initial goal queue, while tac1 searches it.
   57.49 @@ -138,7 +138,7 @@
   57.50    to suppress solutions arising from earlier searches, as the accumulated cost
   57.51    (k) can be wrong.*)
   57.52  fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
   57.53 - let val countr = ref 0
   57.54 + let val countr = Unsynchronized.ref 0
   57.55       and tf = tracify trace_DEPTH_FIRST (tac1 1)
   57.56       and qs0 = tac0 st
   57.57       (*bnd = depth bound; inc = estimate of increment required next*)
   57.58 @@ -156,7 +156,7 @@
   57.59         | depth (bnd,inc) ((k,np,rgd,q)::qs) =
   57.60            if k>=bnd then depth (bnd,inc) qs
   57.61            else
   57.62 -          case (countr := !countr+1;
   57.63 +          case (Unsynchronized.inc countr;
   57.64                  if !trace_DEPTH_FIRST then
   57.65                      tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
   57.66                  else ();
   57.67 @@ -199,7 +199,7 @@
   57.68  
   57.69  (*** Best-first search ***)
   57.70  
   57.71 -val trace_BEST_FIRST = ref false;
   57.72 +val trace_BEST_FIRST = Unsynchronized.ref false;
   57.73  
   57.74  (*For creating output sequence*)
   57.75  fun some_of_list []     = NONE
   57.76 @@ -273,7 +273,7 @@
   57.77  fun some_of_list []     = NONE
   57.78    | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
   57.79  
   57.80 -val trace_ASTAR = ref false;
   57.81 +val trace_ASTAR = Unsynchronized.ref false;
   57.82  
   57.83  fun THEN_ASTAR tac0 (satp, costf) tac1 =
   57.84    let val tf = tracify trace_ASTAR tac1;
    58.1 --- a/src/Pure/simplifier.ML	Tue Sep 29 11:48:32 2009 +0200
    58.2 +++ b/src/Pure/simplifier.ML	Tue Sep 29 11:49:22 2009 +0200
    58.3 @@ -32,7 +32,7 @@
    58.4    include BASIC_SIMPLIFIER
    58.5    val pretty_ss: Proof.context -> simpset -> Pretty.T
    58.6    val clear_ss: simpset -> simpset
    58.7 -  val debug_bounds: bool ref
    58.8 +  val debug_bounds: bool Unsynchronized.ref
    58.9    val inherit_context: simpset -> simpset -> simpset
   58.10    val the_context: simpset -> Proof.context
   58.11    val context: Proof.context -> simpset -> simpset
   58.12 @@ -424,5 +424,5 @@
   58.13  
   58.14  end;
   58.15  
   58.16 -structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
   58.17 -open BasicSimplifier;
   58.18 +structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
   58.19 +open Basic_Simplifier;
    59.1 --- a/src/Pure/tactical.ML	Tue Sep 29 11:48:32 2009 +0200
    59.2 +++ b/src/Pure/tactical.ML	Tue Sep 29 11:49:22 2009 +0200
    59.3 @@ -34,9 +34,9 @@
    59.4    val RANGE: (int -> tactic) list -> int -> tactic
    59.5    val print_tac: string -> tactic
    59.6    val pause_tac: tactic
    59.7 -  val trace_REPEAT: bool ref
    59.8 -  val suppress_tracing: bool ref
    59.9 -  val tracify: bool ref -> tactic -> tactic
   59.10 +  val trace_REPEAT: bool Unsynchronized.ref
   59.11 +  val suppress_tracing: bool Unsynchronized.ref
   59.12 +  val tracify: bool Unsynchronized.ref -> tactic -> tactic
   59.13    val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic
   59.14    val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic
   59.15    val REPEAT_DETERM_N: int -> tactic -> tactic
   59.16 @@ -204,16 +204,16 @@
   59.17  and TRACE_QUIT;
   59.18  
   59.19  (*Tracing flags*)
   59.20 -val trace_REPEAT= ref false
   59.21 -and suppress_tracing = ref false;
   59.22 +val trace_REPEAT= Unsynchronized.ref false
   59.23 +and suppress_tracing = Unsynchronized.ref false;
   59.24  
   59.25  (*Handle all tracing commands for current state and tactic *)
   59.26  fun exec_trace_command flag (tac, st) =
   59.27     case TextIO.inputLine TextIO.stdIn of
   59.28         SOME "\n" => tac st
   59.29       | SOME "f\n" => Seq.empty
   59.30 -     | SOME "o\n" => (flag:=false;  tac st)
   59.31 -     | SOME "s\n" => (suppress_tracing:=true;  tac st)
   59.32 +     | SOME "o\n" => (flag := false;  tac st)
   59.33 +     | SOME "s\n" => (suppress_tracing := true;  tac st)
   59.34       | SOME "x\n" => (tracing "Exiting now";  raise (TRACE_EXIT st))
   59.35       | SOME "quit\n" => raise TRACE_QUIT
   59.36       | _     => (tracing
    60.1 --- a/src/Pure/term.ML	Tue Sep 29 11:48:32 2009 +0200
    60.2 +++ b/src/Pure/term.ML	Tue Sep 29 11:49:22 2009 +0200
    60.3 @@ -112,7 +112,7 @@
    60.4    val exists_type: (typ -> bool) -> term -> bool
    60.5    val exists_subterm: (term -> bool) -> term -> bool
    60.6    val exists_Const: (string * typ -> bool) -> term -> bool
    60.7 -  val show_question_marks: bool ref
    60.8 +  val show_question_marks: bool Unsynchronized.ref
    60.9  end;
   60.10  
   60.11  signature TERM =
   60.12 @@ -963,7 +963,7 @@
   60.13  
   60.14  (* display variables *)
   60.15  
   60.16 -val show_question_marks = ref true;
   60.17 +val show_question_marks = Unsynchronized.ref true;
   60.18  
   60.19  fun string_of_vname (x, i) =
   60.20    let
    61.1 --- a/src/Pure/term_subst.ML	Tue Sep 29 11:48:32 2009 +0200
    61.2 +++ b/src/Pure/term_subst.ML	Tue Sep 29 11:49:22 2009 +0200
    61.3 @@ -157,28 +157,32 @@
    61.4  in
    61.5  
    61.6  fun instantiateT_maxidx instT ty i =
    61.7 -  let val maxidx = ref i
    61.8 +  let val maxidx = Unsynchronized.ref i
    61.9    in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
   61.10  
   61.11  fun instantiate_maxidx insts tm i =
   61.12 -  let val maxidx = ref i
   61.13 +  let val maxidx = Unsynchronized.ref i
   61.14    in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
   61.15  
   61.16  fun instantiateT [] ty = ty
   61.17    | instantiateT instT ty =
   61.18 -      (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle Same.SAME => ty);
   61.19 +      (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
   61.20 +        handle Same.SAME => ty);
   61.21  
   61.22  fun instantiate ([], []) tm = tm
   61.23    | instantiate insts tm =
   61.24 -      (instantiate_same (ref ~1) (no_indexes2 insts) tm handle Same.SAME => tm);
   61.25 +      (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
   61.26 +        handle Same.SAME => tm);
   61.27  
   61.28  fun instantiateT_option [] _ = NONE
   61.29    | instantiateT_option instT ty =
   61.30 -      (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle Same.SAME => NONE);
   61.31 +      (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
   61.32 +        handle Same.SAME => NONE);
   61.33  
   61.34  fun instantiate_option ([], []) _ = NONE
   61.35    | instantiate_option insts tm =
   61.36 -      (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle Same.SAME => NONE);
   61.37 +      (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
   61.38 +        handle Same.SAME => NONE);
   61.39  
   61.40  end;
   61.41  
    62.1 --- a/src/Pure/type.ML	Tue Sep 29 11:48:32 2009 +0200
    62.2 +++ b/src/Pure/type.ML	Tue Sep 29 11:49:22 2009 +0200
    62.3 @@ -417,8 +417,8 @@
    62.4  (*order-sorted unification*)
    62.5  fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
    62.6    let
    62.7 -    val tyvar_count = ref maxidx;
    62.8 -    fun gen_tyvar S = TVar ((Name.aT, inc tyvar_count), S);
    62.9 +    val tyvar_count = Unsynchronized.ref maxidx;
   62.10 +    fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S);
   62.11  
   62.12      fun mg_domain a S = Sorts.mg_domain classes a S
   62.13        handle Sorts.CLASS_ERROR _ => raise TUNIFY;
    63.1 --- a/src/Pure/unify.ML	Tue Sep 29 11:48:32 2009 +0200
    63.2 +++ b/src/Pure/unify.ML	Tue Sep 29 11:49:22 2009 +0200
    63.3 @@ -106,7 +106,7 @@
    63.4    the occurs check must ignore the types of variables. This avoids
    63.5    that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
    63.6    substitution when ?'a is instantiated with T later. *)
    63.7 -fun occurs_terms (seen: (indexname list) ref,
    63.8 +fun occurs_terms (seen: (indexname list) Unsynchronized.ref,
    63.9        env: Envir.env, v: indexname, ts: term list): bool =
   63.10    let fun occurs [] = false
   63.11    | occurs (t::ts) =  occur t  orelse  occurs ts
   63.12 @@ -160,7 +160,7 @@
   63.13  Warning: finds a rigid occurrence of ?f in ?f(t).
   63.14    Should NOT be called in this case: there is a flex-flex unifier
   63.15  *)
   63.16 -fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
   63.17 +fun rigid_occurs_term (seen: (indexname list) Unsynchronized.ref, env, v: indexname, t) =
   63.18    let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
   63.19             else NoOcc
   63.20        fun occurs [] = NoOcc
   63.21 @@ -230,7 +230,7 @@
   63.22    If v occurs nonrigidly then must use full algorithm. *)
   63.23  fun assignment thy (env, rbinder, t, u) =
   63.24      let val vT as (v,T) = get_eta_var (rbinder, 0, t)
   63.25 -    in  case rigid_occurs_term (ref [], env, v, u) of
   63.26 +    in  case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
   63.27          NoOcc => let val env = unify_types thy (body_type env T,
   63.28               fastype env (rbinder,u),env)
   63.29      in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
   63.30 @@ -429,7 +429,7 @@
   63.31    Attempts to update t with u, raising ASSIGN if impossible*)
   63.32  fun ff_assign thy (env, rbinder, t, u) : Envir.env =
   63.33  let val vT as (v,T) = get_eta_var(rbinder,0,t)
   63.34 -in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
   63.35 +in if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
   63.36     else let val env = unify_types thy (body_type env T,
   63.37            fastype env (rbinder,u),
   63.38            env)