# HG changeset patch
# User blanchet
# Date 1376315337 -7200
# Node ID 3e0fe71f3ce14014447502b06600f502d5c391f8
# Parent  f2df0730f8ac3fc45ddb84517487b732cba3d0cf
tuned messages

diff -r f2df0730f8ac -r 3e0fe71f3ce1 src/HOL/Tools/try0.ML
--- 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"