1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -329,8 +329,8 @@
     1.4      Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
     1.5    | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
     1.6    | Normal => if blocking then quote name ^ " found a proof"
     1.7 -              else "Try this command"
     1.8 -  | Minimize => "Try this command"
     1.9 +              else "Try this"
    1.10 +  | Minimize => "Try this"
    1.11  
    1.12  val smt_triggers =
    1.13    Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)