1.1 --- a/src/Pure/General/file.ML	Tue Oct 27 13:15:20 2009 +0100
     1.2 +++ b/src/Pure/General/file.ML	Tue Oct 27 13:16:16 2009 +0100
     1.3 @@ -90,10 +90,10 @@
     1.4      Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
     1.5  in
     1.6  
     1.7 -fun check_cache (path, time) = CRITICAL (fn () =>
     1.8 +fun check_cache (path, time) =
     1.9    (case Symtab.lookup (! ident_cache) path of
    1.10      NONE => NONE
    1.11 -  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
    1.12 +  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
    1.13  
    1.14  fun update_cache (path, (time, id)) = CRITICAL (fn () =>
    1.15    Unsynchronized.change ident_cache

     2.1 --- a/src/Pure/General/print_mode.ML	Tue Oct 27 13:15:20 2009 +0100
     2.2 +++ b/src/Pure/General/print_mode.ML	Tue Oct 27 13:16:16 2009 +0100
     2.3 @@ -35,7 +35,7 @@
     2.4    let val modes =
     2.5      (case Thread.getLocal tag of
     2.6        SOME (SOME modes) => modes
     2.7 -    | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
     2.8 +    | _ => ! print_mode)
     2.9    in subtract (op =) [input, internal] modes end;
    2.10  
    2.11  fun print_mode_active mode = member (op =) (print_mode_value ()) mode;

     3.1 --- a/src/Pure/Isar/isar_document.ML	Tue Oct 27 13:15:20 2009 +0100
     3.2 +++ b/src/Pure/Isar/isar_document.ML	Tue Oct 27 13:16:16 2009 +0100
     3.3 @@ -119,13 +119,13 @@
     3.4  in
     3.5  
     3.6  fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
     3.7 -fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
     3.8 +fun get_states () = ! global_states;
     3.9  
    3.10  fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
    3.11 -fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
    3.12 +fun get_commands () = ! global_commands;
    3.13  
    3.14  fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
    3.15 -fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
    3.16 +fun get_documents () = ! global_documents;
    3.17  
    3.18  fun init () = NAMED_CRITICAL "Isar" (fn () =>
    3.19   (global_states := Symtab.empty;

     4.1 --- a/src/Pure/Isar/outer_keyword.ML	Tue Oct 27 13:15:20 2009 +0100
     4.2 +++ b/src/Pure/Isar/outer_keyword.ML	Tue Oct 27 13:16:16 2009 +0100
     4.3 @@ -121,8 +121,8 @@
     4.4  
     4.5  in
     4.6  
     4.7 -fun get_commands () = CRITICAL (fn () => ! global_commands);
     4.8 -fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
     4.9 +fun get_commands () = ! global_commands;
    4.10 +fun get_lexicons () = ! global_lexicons;
    4.11  
    4.12  fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
    4.13  fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);

     5.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Oct 27 13:15:20 2009 +0100
     5.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Oct 27 13:16:16 2009 +0100
     5.3 @@ -101,8 +101,8 @@
     5.4  
     5.5  (* access current syntax *)
     5.6  
     5.7 -fun get_commands () = CRITICAL (fn () => ! global_commands);
     5.8 -fun get_markups () = CRITICAL (fn () => ! global_markups);
     5.9 +fun get_commands () = ! global_commands;
    5.10 +fun get_markups () = ! global_markups;
    5.11  
    5.12  fun get_command () = Symtab.lookup (get_commands ());
    5.13  fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));

     6.1 --- a/src/Pure/Isar/toplevel.ML	Tue Oct 27 13:15:20 2009 +0100
     6.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Oct 27 13:16:16 2009 +0100
     6.3 @@ -552,7 +552,7 @@
     6.4  local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
     6.5  
     6.6  fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
     6.7 -fun get_hooks () = CRITICAL (fn () => ! hooks);
     6.8 +fun get_hooks () = ! hooks;
     6.9  
    6.10  end;
    6.11  

     7.1 --- a/src/Pure/System/isar.ML	Tue Oct 27 13:15:20 2009 +0100
     7.2 +++ b/src/Pure/System/isar.ML	Tue Oct 27 13:16:16 2009 +0100
     7.3 @@ -47,10 +47,10 @@
     7.4        | edit n (st, hist) = edit (n - 1) (f st hist);
     7.5    in edit count (! global_state, ! global_history) end);
     7.6  
     7.7 -fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
     7.8 +fun state () = ! global_state;
     7.9  
    7.10 -fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
    7.11 -fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
    7.12 +fun exn () = ! global_exn;
    7.13 +fun set_exn exn =  global_exn := exn;
    7.14  
    7.15  end;
    7.16