# HG changeset patch
# User wenzelm
# Date 953843803 -3600
# Node ID 2675e2f4dc61200cbe9ae386e91bbfcd6ecf38ab
# Parent  2278de8bde59be15446142b5b6a932bef3d668c9
tuned output;

diff -r 2278de8bde59 -r 2675e2f4dc61 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Mar 23 11:28:10 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Mar 23 21:36:43 2000 +0100
@@ -329,8 +329,9 @@
       else [];
 
     val prts =
-     [Pretty.str ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
-        ", depth " ^ string_of_int (length nodes div 2)), Pretty.str ""] @
+     [Pretty.str ("proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
+        (if ! verbose then ", depth " ^ string_of_int (length nodes div 2)
+        else "")), Pretty.str ""] @
      (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
      (if ! verbose orelse mode = Forward then
        (pretty_facts "" facts @ pretty_goal (find_goal 0 state))
diff -r 2278de8bde59 -r 2675e2f4dc61 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Mar 23 11:28:10 2000 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Mar 23 21:36:43 2000 +0100
@@ -80,7 +80,7 @@
   | str_of_node (Proof _) = "in proof mode";
 
 fun print_ctxt thy = Pretty.writeln (Pretty.block
-  [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
+  [Pretty.str "theory", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
     Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]);
 
 fun print_node_ctxt (Theory thy) = print_ctxt thy