--- a/src/Pure/General/output.ML Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Pure/General/output.ML Mon Sep 17 16:36:41 2007 +0200
@@ -67,7 +67,7 @@
fun add_mode name output escape = CRITICAL (fn () =>
change modes (Symtab.update_new (name, {output = output, escape = escape})));
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_width x = #output (get_mode ()) x;