added with_modes, with_default;

--- a/src/Pure/General/print_mode.ML	Mon Jul 23 16:45:01 2007 +0200
+++ b/src/Pure/General/print_mode.ML	Mon Jul 23 16:45:02 2007 +0200
@@ -6,18 +6,31 @@
 mechanisms.
 *)
 
-signature PRINT_MODE =
+signature BASIC_PRINT_MODE =
 sig
   val print_mode: string list ref
   val print_mode_active: string -> bool
 end;
 
+signature PRINT_MODE =
+sig
+  include BASIC_PRINT_MODE
+  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
+  val with_default: ('a -> 'b) -> 'a -> 'b
+end;
+
 structure PrintMode: PRINT_MODE =
 struct
 
 val print_mode = ref ([]: string list);
 fun print_mode_active s = member (op =) (! print_mode) s;
 
+fun with_modes modes f x = CRITICAL (fn () =>
+  setmp print_mode (modes @ ! print_mode) f x);
+
+fun with_default f x = setmp print_mode [] f x;
+
 end;
 
-open PrintMode;
+structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
+open BasicPrintMode;

--- a/src/Pure/Tools/nbe.ML	Mon Jul 23 16:45:01 2007 +0200
+++ b/src/Pure/Tools/nbe.ML	Mon Jul 23 16:45:02 2007 +0200
@@ -190,7 +190,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 = 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;