diff -r 5106e13d400f -r 34927a1e0ae8 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Fri Apr 03 18:03:29 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Sat Apr 04 20:22:39 2009 +0200
@@ -15,7 +15,7 @@
   val strip_prefix: string -> string -> string option
   val setup: Context.theory -> Context.theory
   (* extracting lemma list*)
-  val find_failure_e_vamp_spass: string -> string option
+  val find_failure: string -> string option
   val lemma_list_dfg: string * string vector * Proof.context * Thm.thm * int -> string
   val lemma_list_tstp: string * string vector * Proof.context * Thm.thm * int -> string
   (* structured proofs *)
@@ -459,14 +459,16 @@
     
   (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
   
-  val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable","SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
+  val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
+    "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
   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 =
+  val failure_strings_SPASS = ["SPASS beiseite: Completion found.",
+    "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."];
+  val failure_strings_remote = ["Remote-script could not extract proof"];
+  fun find_failure 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)
+         (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
     in if null failures then NONE else SOME (hd failures) end;
     
   (*=== EXTRACTING PROOF-TEXT === *)