# HG changeset patch
# User mengj
# Date 1141700051 -3600
# Node ID e0b483dea2c0b79faa360cc42567f40455212aad
# Parent  7681c04d8bffaf41b2148932d9879f68c7f2fae2
Moved the settings for ATP time limit to res_atp.ML

diff -r 7681c04d8bff -r e0b483dea2c0 src/HOL/Tools/res_atp_provers.ML
--- a/src/HOL/Tools/res_atp_provers.ML	Tue Mar 07 03:51:40 2006 +0100
+++ b/src/HOL/Tools/res_atp_provers.ML	Tue Mar 07 03:54:11 2006 +0100
@@ -22,39 +22,36 @@
 
 local 
 
-fun locations [] = ()
-|   locations (s::ss) = (warning s; locations ss);
+fun location s = warning ("ATP input at: " ^ s);
 
 in 
 
-fun call_vampire (files:string list, time: int) = 
-  let val _ = locations files
-      val output = (space_implode " " files) ^ "  "
+fun call_vampire (file:string, time: int) = 
+  let val _ = location file
       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])
+      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,file])
       val (instr,outstr) = Unix.streamsOf ch
   in if_proof_vampire instr
   end;
 
-fun call_eprover (files:string list, time:int) =
-  let val _ = locations files
-      val output = (space_implode " " files) ^ "  "
+fun call_eprover (file:string, time:int) =
+  let val _ = location file
       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])
+      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",file])
       val (instr,outstr) = Unix.streamsOf ch
   in if_proof_E instr
   end; 
 
 end
 
-fun vampire_o thy ((helper,files),time) = (if (call_vampire (helper @ files,time)) then (warning (hd files); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
-  else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
+fun vampire_o thy (file,time) = (if (call_vampire (file,time)) then (warning file; ResAtp.cond_rm_tmp file;HOLogic.mk_Trueprop HOLogic.false_const)  
+				 else (ResAtp.cond_rm_tmp file;raise Fail ("vampire oracle failed")));
 
 
-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 (ResAtpSetup.cond_rm_tmp files;raise Fail ("eprover oracle failed")));
+fun eprover_o thy (file,time) = (if (call_eprover (file,time)) then (warning file; ResAtp.cond_rm_tmp file;HOLogic.mk_Trueprop HOLogic.false_const)
+				 else (ResAtp.cond_rm_tmp file;raise Fail ("eprover oracle failed")));
 
 end;