tuned print_result;

--- a/src/Pure/Isar/isar_thy.ML	Thu Sep 23 18:42:28 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Sep 23 19:22:52 1999 +0200
@@ -342,7 +342,7 @@
 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 =