1.1 --- a/src/Tools/nbe.ML	Mon Sep 17 16:06:35 2007 +0200
     1.2 +++ b/src/Tools/nbe.ML	Mon Sep 17 16:36:41 2007 +0200
     1.3 @@ -373,7 +373,7 @@
     1.4      val ct = Thm.cterm_of thy t;
     1.5      val (_, t') = (Logic.dest_equals o Thm.prop_of o normalization_conv) ct;
     1.6      val ty = Term.type_of t';
     1.7 -    val p = Library.setmp print_mode (modes @ ! print_mode) (fn () =>
     1.8 +    val p = Library.setmp print_mode (modes @ print_mode_value ()) (fn () =>
     1.9        Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
    1.10          Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
    1.11    in Pretty.writeln p end;