src/Pure/Isar/isar_thy.ML
changeset 7590 76c9e71d491a
parent 7572 6e6dafacbc28
child 7614 88392b7bc549
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Sep 23 18:42:28 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Sep 23 19:22:52 1999 +0200
     1.3 @@ -342,7 +342,7 @@
     1.4  local
     1.5  
     1.6  fun pretty_result {kind, name, thm} =
     1.7 -  Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name ^ ":")),
     1.8 +  Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name) ^ ":"),
     1.9      Pretty.fbrk, Proof.pretty_thm thm];
    1.10  
    1.11  fun pretty_rule thm =