# HG changeset patch
# User immler@in.tum.de
# Date 1235144897 -3600
# Node ID d8b6542e643f2f0160620860ead211fa0ae22c64
# Parent  03b46412760e7ee1c1542435e6fffc89e0cd364e# Parent  76b58a07e704072e4b9784caddff15749ac2f353
merged

diff -r 03b46412760e -r d8b6542e643f src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Fri Feb 20 14:49:39 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Fri Feb 20 16:48:17 2009 +0100
@@ -78,10 +78,14 @@
     val failure = find_failure proof
     val success = rc = 0 andalso is_none failure
     val message =
-      if isSome failure then "Could not prove: " ^ the failure
-      else if rc <> 0
-      then "Exited with return code " ^ string_of_int rc ^ ": " ^ proof 
-      else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
+      if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
+      else "Could not prove goal."
+    val _ = if isSome failure
+      then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
+      else ()
+    val _ = if rc <> 0
+      then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
+      else ()
   in (success, message) end;