# HG changeset patch
# User mengj
# Date 1132294026 -3600
# Node ID 02f1c40224846aadd15c0240a4538adf3d985ac1
# Parent  971dc74390881f2e89992519f001bc22494b05b8
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).

diff -r 971dc7439088 -r 02f1c4022484 src/HOL/Tools/res_atp_provers.ML
--- a/src/HOL/Tools/res_atp_provers.ML	Fri Nov 18 07:06:07 2005 +0100
+++ b/src/HOL/Tools/res_atp_provers.ML	Fri Nov 18 07:07:06 2005 +0100
@@ -39,11 +39,11 @@
 
 
 
-fun vampire_o thy (files,time) = (if (call_vampire (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
+fun vampire_o thy ((helper,files),time) = (if (call_vampire (helper @ files,time)) then (warning (hd helper); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
   else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
 
 
-fun eprover_o thy (files,time) = (if (call_eprover (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
+fun eprover_o thy ((helper,files),time) = (if (call_eprover (helper @ files,time)) then (warning (hd helper); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
   else (raise Fail ("eprover oracle failed")));
 
 end;