ProofContext.setmp_verbose_CRITICAL;

--- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 27 13:16:16 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 27 13:24:40 2009 +0100
@@ -333,14 +333,14 @@
   Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of);
 
 val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose
+  ProofContext.setmp_verbose_CRITICAL
     ProofContext.print_lthms (Toplevel.context_of state));
 
 val print_configs = Toplevel.unknown_context o Toplevel.keep (fn state =>
   Attrib.print_configs (Toplevel.context_of state));
 
 val print_theorems_proof = Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose
+  ProofContext.setmp_verbose_CRITICAL
     ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
 
 val print_theorems_theory = Toplevel.keep (fn state =>
@@ -431,10 +431,10 @@
 (* print proof context contents *)
 
 val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state));
+  ProofContext.setmp_verbose_CRITICAL ProofContext.print_binds (Toplevel.context_of state));
 
 val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose ProofContext.print_cases (Toplevel.context_of state));
+  ProofContext.setmp_verbose_CRITICAL ProofContext.print_cases (Toplevel.context_of state));
 
 
 (* print theorems, terms, types etc. *)

--- a/src/Pure/Isar/proof_context.ML	Tue Oct 27 13:16:16 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 27 13:24:40 2009 +0100
@@ -122,7 +122,7 @@
   val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
   val verbose: bool Unsynchronized.ref
-  val setmp_verbose: ('a -> 'b) -> 'a -> 'b
+  val setmp_verbose_CRITICAL: ('a -> 'b) -> 'a -> 'b
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
   val print_binds: Proof.context -> unit
@@ -1200,7 +1200,7 @@
 val verbose = Unsynchronized.ref false;
 fun verb f x = if ! verbose then f (x ()) else [];
 
-fun setmp_verbose f x = setmp_CRITICAL verbose true f x;
+fun setmp_verbose_CRITICAL f x = setmp_CRITICAL verbose true f x;
 
 
 (* local syntax *)