# HG changeset patch
# User mengj
# Date 1133158452 -3600
# Node ID 4f0904ba19c2caf63101a2037914c38ea85d31a6
# Parent  0e9a851db989db9c34c02569eaa6812739824780
Slight modification to trace information.

diff -r 0e9a851db989 -r 4f0904ba19c2 src/HOL/Tools/res_atp_provers.ML
--- a/src/HOL/Tools/res_atp_provers.ML	Mon Nov 28 07:13:43 2005 +0100
+++ b/src/HOL/Tools/res_atp_provers.ML	Mon Nov 28 07:14:12 2005 +0100
@@ -39,11 +39,11 @@
 
 
 
-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)  
+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 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)
+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")));
 
 end;