--- 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
--- 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.",