# HG changeset patch
# User immler@in.tum.de
# Date 1235144881 -3600
# Node ID 76b58a07e704072e4b9784caddff15749ac2f353
# Parent  1baeda435aa61b968963b41254c44e4b294e6ca6
changed message

diff -r 1baeda435aa6 -r 76b58a07e704 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Fri Feb 20 11:04:18 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Fri Feb 20 16:48:01 2009 +0100
@@ -79,7 +79,7 @@
     val success = rc = 0 andalso is_none failure
     val message =
       if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
-      else "Could not prove."
+      else "Could not prove goal."
     val _ = if isSome failure
       then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
       else ()