src/Tools/nbe.ML
changeset 24612 d1b315bdb8d7
parent 24590 733120d04233
child 24634 38db11874724
--- a/src/Tools/nbe.ML	Mon Sep 17 16:06:35 2007 +0200
+++ b/src/Tools/nbe.ML	Mon Sep 17 16:36:41 2007 +0200
@@ -373,7 +373,7 @@
     val ct = Thm.cterm_of thy t;
     val (_, t') = (Logic.dest_equals o Thm.prop_of o normalization_conv) ct;
     val ty = Term.type_of t';
-    val p = Library.setmp print_mode (modes @ ! print_mode) (fn () =>
+    val p = Library.setmp print_mode (modes @ print_mode_value ()) (fn () =>
       Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
   in Pretty.writeln p end;