# HG changeset patch
# User wenzelm
# Date 938107372 -7200
# Node ID 76c9e71d491a6359d147939f04a4eb1bb34174a8
# Parent  59663b367833b48bc1efab9114ad2b615dedd156
tuned print_result;

diff -r 59663b367833 -r 76c9e71d491a src/Pure/Isar/isar_thy.ML
--- 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 =