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