src/Pure/Isar/outer_syntax.ML
changeset 32738 15bb09ca0378
parent 30573 49899f26fbd1
child 33223 d27956b4d3b4
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -88,11 +88,11 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val global_commands = ref (Symtab.empty: command Symtab.table);
     1.8 -val global_markups = ref ([]: (string * ThyOutput.markup) list);
     1.9 +val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
    1.10 +val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
    1.11  
    1.12  fun change_commands f = CRITICAL (fn () =>
    1.13 - (change global_commands f;
    1.14 + (Unsynchronized.change global_commands f;
    1.15    global_markups :=
    1.16      Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
    1.17        (! global_commands) []));