--- 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))