added some debugging code.

--- a/src/HOL/Tools/res_atp_provers.ML	Fri Jan 20 04:35:23 2006 +0100
+++ b/src/HOL/Tools/res_atp_provers.ML	Fri Jan 20 04:50:01 2006 +0100
@@ -19,6 +19,13 @@
   else if (thisLine = "") then false
   else if_proof_E instr end;		
 
+local 
+
+fun locations [] = ()
+|   locations (s::ss) = (warning s; locations ss);
+
+in 
+
 fun call_vampire (files:string list, time: int) = 
   let val output = (space_implode " " files) ^ "  "
       val runtime = "-t " ^ (string_of_int time)
@@ -37,7 +44,7 @@
   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")));