# HG changeset patch
# User wenzelm
# Date 1239802033 -7200
# Node ID ec3f33437fe396a24ff524a1d334dbc05221587a
# Parent  bad26d8f0adf0bae98d0e45bd796efe83006d8d9
more generic error message, which also covers more fundamental failure;

diff -r bad26d8f0adf -r ec3f33437fe3 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Wed Apr 15 11:14:48 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Wed Apr 15 15:27:13 2009 +0200
@@ -79,14 +79,16 @@
     val failure = find_failure proof
     val success = rc = 0 andalso is_none failure
     val message =
-      if isSome failure then "Proof attempt failed."
-      else if rc <> 0 then "Proof attempt failed: " ^ proof
+      if is_some failure then "External prover failed."
+      else if rc <> 0 then "External prover failed: " ^ proof
       else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, th, subgoalno)
 
-    val _ = if isSome failure
+    val _ =
+      if is_some failure
       then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
       else ()
-    val _ = if rc <> 0
+    val _ =
+      if rc <> 0
       then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
       else ()
   in (success, message) end;