1.1 --- a/src/Pure/General/pretty.ML Mon Sep 17 16:06:35 2007 +0200
1.2 +++ b/src/Pure/General/pretty.ML Mon Sep 17 16:36:41 2007 +0200
1.3 @@ -93,7 +93,7 @@
1.4 fun add_mode name indent = CRITICAL (fn () =>
1.5 change modes (Symtab.update_new (name, {indent = indent})));
1.6 fun get_mode () =
1.7 - the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
1.8 + the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
1.9 end;
1.10
1.11 fun mode_indent x y = #indent (get_mode ()) x y;