author | wenzelm |
Wed, 25 Aug 1999 20:39:50 +0200 | |
changeset 7353 | b5a5abea1559 |
parent 7352 | d98001b492b3 |
child 7354 | 358b1c5391f0 |
--- a/src/Pure/Isar/isar_thy.ML Wed Aug 25 20:39:18 1999 +0200 +++ b/src/Pure/Isar/isar_thy.ML Wed Aug 25 20:39:50 1999 +0200 @@ -339,7 +339,7 @@ Pretty.block [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Proof.pretty_thm thm]; fun pretty_rule thm = - Pretty.block [Pretty.str "solving goal by rule:", Pretty.fbrk, Proof.pretty_thm thm]; + Pretty.block [Pretty.str "trying to solve goal by rule:", Pretty.fbrk, Proof.pretty_thm thm]; val print_result = Pretty.writeln o pretty_result;