# HG changeset patch
# User wenzelm
# Date 954094348 -7200
# Node ID 3051aa8aa412302f11f511595881ef73d8027316
# Parent  5c7ed2af8bfbd0d2c68d9979d7835f28ccf120d9
tuned output;

diff -r 5c7ed2af8bfb -r 3051aa8aa412 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Mar 26 20:11:12 2000 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Mar 26 20:12:28 2000 +0200
@@ -329,7 +329,7 @@
       else [];
 
     val prts =
-     [Pretty.str ("proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
+     [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 ""]) @