src/Pure/Isar/isar_thy.ML

 (* print result *)
 
 local
 
 fun pretty_result {kind, name, thm} =
-  Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name ^ ":")),
+  Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name) ^ ":"),
     Pretty.fbrk, Proof.pretty_thm thm];
 
 fun pretty_rule thm =
   Pretty.block [Pretty.str "trying to solve goal by rule:", Pretty.fbrk, Proof.pretty_thm thm];