diff -r e1172791ad0d -r e437d47f419f src/HOL/Tools/try_methods.ML
--- a/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
@@ -136,7 +136,7 @@
           (case mode of
              Auto_Try => "Auto Try Methods found a proof"
            | Try => "Try Methods found a proof"
-           | Normal => "Try this command") ^ ": " ^
+           | Normal => "Try this") ^ ": " ^
           Markup.markup Markup.sendback
               ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
                 else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^