src/HOL/Tools/res_atp_provers.ML
changeset 18196 02f1c4022484
parent 17907 c20e4bddcb11
child 18272 4f0904ba19c2
     1.1 --- a/src/HOL/Tools/res_atp_provers.ML	Fri Nov 18 07:06:07 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_atp_provers.ML	Fri Nov 18 07:07:06 2005 +0100
     1.3 @@ -39,11 +39,11 @@
     1.4  
     1.5  
     1.6  
     1.7 -fun vampire_o thy (files,time) = (if (call_vampire (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
     1.8 +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)  
     1.9    else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
    1.10  
    1.11  
    1.12 -fun eprover_o thy (files,time) = (if (call_eprover (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
    1.13 +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)
    1.14    else (raise Fail ("eprover oracle failed")));
    1.15  
    1.16  end;