--- a/src/HOL/Tools/try0.ML Mon Aug 12 15:25:17 2013 +0200
+++ b/src/HOL/Tools/try0.ML Mon Aug 12 15:48:57 2013 +0200
@@ -134,8 +134,8 @@
val need_parens = exists_string (curry (op =) " ") s
val message =
(case mode of
- Auto_Try => "Auto Try Methods found a proof"
- | Try => "Try Methods found a proof"
+ Auto_Try => "Auto Try0 found a proof"
+ | Try => "Try0 found a proof"
| Normal => "Try this") ^ ": " ^
Active.sendback_markup (if mode = Auto_Try then [Markup.padding_command] else [])
((if nprems_of (#goal (Proof.goal st)) = 1 then "by"