1.1 --- a/src/HOL/Tools/atp_wrapper.ML	Fri Feb 20 11:04:18 2009 +0100
     1.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Fri Feb 20 16:48:01 2009 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4      val success = rc = 0 andalso is_none failure
     1.5      val message =
     1.6        if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
     1.7 -      else "Could not prove."
     1.8 +      else "Could not prove goal."
     1.9      val _ = if isSome failure
    1.10        then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
    1.11        else ()