Slight modification to trace information.
authormengj
Mon Nov 28 07:14:12 2005 +0100 (2005-11-28)
changeset 182724f0904ba19c2
parent 18271 0e9a851db989
child 18273 e15a825da262
Slight modification to trace information.
src/HOL/Tools/res_atp_provers.ML
     1.1 --- a/src/HOL/Tools/res_atp_provers.ML	Mon Nov 28 07:13:43 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_atp_provers.ML	Mon Nov 28 07:14:12 2005 +0100
     1.3 @@ -39,11 +39,11 @@
     1.4  
     1.5  
     1.6  
     1.7 -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.8 +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)  
     1.9    else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
    1.10  
    1.11  
    1.12 -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.13 +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)
    1.14    else (raise Fail ("eprover oracle failed")));
    1.15  
    1.16  end;