src/Pure/General/pretty.ML
changeset 24612 d1b315bdb8d7
parent 23922 707639e9497d
child 26703 c07b1a90600c
     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;