# HG changeset patch
# User wenzelm
# Date 930954197 -7200
# Node ID 7bb02d03035d735e2aceb9e7397c368a0589d61a
# Parent  05732285677e3c6999a7371c01cc7a6a13bd23f5
tuned print_state;

diff -r 05732285677e -r 7bb02d03035d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Jul 03 00:22:53 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Jul 03 00:23:17 1999 +0200
@@ -19,6 +19,7 @@
   val goal_facts: (state -> thm list) -> state -> state
   val use_facts: state -> state
   val reset_facts: state -> state
+  val assert_forward: state -> state
   val assert_backward: state -> state
   val enter_forward: state -> state
   val verbose: bool ref
@@ -280,7 +281,7 @@
 
     val ctxt_strings = ProofContext.strings_of_context context;
   in
-    writeln ("Nesting level: " ^ string_of_int (length nodes div 2));
+    if ! verbose then writeln ("Nesting level: " ^ string_of_int (length nodes div 2)) else ();
     writeln "";
     writeln (mode_name mode ^ " mode");
     writeln "";