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