# HG changeset patch
# User immler@in.tum.de
# Date 1232546253 -3600
# Node ID 0f4f36779ca731797bee79b64653ed8447f09cb5
# Parent  7b710756609c4d9ff38e2ad3b1ddcdba2a331da7
tuned;
really find failure

diff -r 7b710756609c -r 0f4f36779ca7 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Tue Jan 20 23:35:37 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Wed Jan 21 14:57:33 2009 +0100
@@ -76,7 +76,7 @@
     
     (* check for success and print out some information on failure *)
     val failure = find_failure proof
-    val success = (rc = 0) andalso (not (isSome failure))
+    val success = rc = 0 andalso is_none failure
     val message =
       if isSome failure then "Could not prove: " ^ the failure
       else if rc <> 0
diff -r 7b710756609c -r 0f4f36779ca7 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Tue Jan 20 23:35:37 2009 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Jan 21 14:57:33 2009 +0100
@@ -463,10 +463,12 @@
   val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
   val failure_strings_SPASS = ["SPASS beiseite: Completion found.","SPASS beiseite: Ran out of time.",
   "SPASS beiseite: Maximal number of loops exceeded."];
-  fun find_failure_e_vamp_spass proof = 
-    hd (map (fn s => if String.isSubstring s proof then SOME s else NONE) 
-            (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS));
-
+  fun find_failure_e_vamp_spass proof =
+    let val failures =
+      map_filter (fn s => if String.isSubstring s proof then SOME s else NONE) 
+         (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS)
+    in if null failures then NONE else SOME (hd failures) end;
+    
   (*=== EXTRACTING PROOF-TEXT === *)
   
   val begin_proof_strings = ["# SZS output start CNFRefutation.",