| changeset 7590 | 76c9e71d491a |
| parent 7572 | 6e6dafacbc28 |
| child 7614 | 88392b7bc549 |
--- 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 =