src/Pure/General/markup.ML
changeset 24612 d1b315bdb8d7
parent 24555 ea220faa69e7
child 24777 c1250851d701
--- a/src/Pure/General/markup.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Pure/General/markup.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -170,7 +170,7 @@
   fun add_mode name output = CRITICAL (fn () =>
     change modes (Symtab.update_new (name, {output = output})));
   fun get_mode () =
-    the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
+    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
 
 fun output ("", _) = ("", "")