src/Pure/Isar/proof.ML

       if ! verbose orelse mode = Forward then ProofContext.pretty_context context
       else if mode = Backward then ProofContext.pretty_prems context
       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 ""]) @
      (if ! verbose orelse mode = Forward then
        (pretty_facts "" facts @ pretty_goal (find_goal 0 state))