# HG changeset patch
# User mengj
# Date 1140695941 -3600
# Node ID b66dff8ab7e9759c0955bb7eb90ad2f290c21436
# Parent  495ecbefc5dfb4f8dd9da6935dcb1953c9dbbe8a
eprover removes tmp files too.

diff -r 495ecbefc5df -r b66dff8ab7e9 src/HOL/Tools/res_atp_provers.ML
--- a/src/HOL/Tools/res_atp_provers.ML	Thu Feb 23 12:57:39 2006 +0100
+++ b/src/HOL/Tools/res_atp_provers.ML	Thu Feb 23 12:59:01 2006 +0100
@@ -19,6 +19,7 @@
   else if (thisLine = "") then false
   else if_proof_E instr end;		
 
+
 local 
 
 fun locations [] = ()
@@ -27,7 +28,8 @@
 in 
 
 fun call_vampire (files:string list, time: int) = 
-  let val output = (space_implode " " files) ^ "  "
+  let val _ = locations files
+      val output = (space_implode " " files) ^ "  "
       val runtime = "-t " ^ (string_of_int time)
       val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
       val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,output])
@@ -36,7 +38,8 @@
   end;
 
 fun call_eprover (files:string list, time:int) =
-  let val output = (space_implode " " files) ^ "  "
+  let val _ = locations files
+      val output = (space_implode " " files) ^ "  "
       val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
       val runtime = "--cpu-limit=" ^ (string_of_int time)
       val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",output])
@@ -51,7 +54,7 @@
 
 
 fun eprover_o thy ((helper,files),time) = (if (call_eprover (helper @ files,time)) then (warning (hd files); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
-  else (raise Fail ("eprover oracle failed")));
+  else (ResAtpSetup.cond_rm_tmp files;raise Fail ("eprover oracle failed")));
 
 end;