src/Pure/Isar/outer_keyword.ML
changeset 32738 15bb09ca0378
parent 30670 9bb872667af6
child 33223 d27956b4d3b4
     1.1 --- a/src/Pure/Isar/outer_keyword.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Isar/outer_keyword.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -116,16 +116,16 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val global_commands = ref (Symtab.empty: T Symtab.table);
     1.8 -val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
     1.9 +val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
    1.10 +val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
    1.11  
    1.12  in
    1.13  
    1.14  fun get_commands () = CRITICAL (fn () => ! global_commands);
    1.15  fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
    1.16  
    1.17 -fun change_commands f = CRITICAL (fn () => change global_commands f);
    1.18 -fun change_lexicons f = CRITICAL (fn () => change global_lexicons f);
    1.19 +fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
    1.20 +fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
    1.21  
    1.22  end;
    1.23