--- a/src/Tools/nbe.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/Tools/nbe.ML Tue Sep 18 18:05:37 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_value ()) (fn () =>
+ val p = PrintMode.with_modes modes (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;