1.1 --- a/src/Pure/General/markup.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -323,10 +323,10 @@
     1.4  
     1.5  local
     1.6    val default = {output = default_output};
     1.7 -  val modes = ref (Symtab.make [("", default)]);
     1.8 +  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
     1.9  in
    1.10    fun add_mode name output = CRITICAL (fn () =>
    1.11 -    change modes (Symtab.update_new (name, {output = output})));
    1.12 +    Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
    1.13    fun get_mode () =
    1.14      the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    1.15  end;