src/HOL/Tools/res_atp.ML

   val eproverLimit: unit -> int
   val spassLimit: unit -> int
   val atp_method: (Proof.context -> thm list -> int -> tactic) ->
     Method.src -> Proof.context -> Proof.method
   val cond_rm_tmp: string -> unit
-  val keep_atp_input: bool ref
   val fol_keep_types: bool ref
   val hol_full_types: unit -> unit
   val hol_partial_types: unit -> unit
   val hol_const_types_only: unit -> unit
   val hol_no_types: unit -> unit

 
 fun vampireLimit () = !vampire_time;
 fun eproverLimit () = !eprover_time;
 fun spassLimit () = !spass_time;
 
-val keep_atp_input = ref false;
 val fol_keep_types = ResClause.keep_types;
 val hol_full_types = ResHolClause.full_types;
 val hol_partial_types = ResHolClause.partial_types;
 val hol_const_types_only = ResHolClause.const_types_only;
 val hol_no_types = ResHolClause.no_types;

     end;
 
 
 (**** remove tmp files ****)
 fun cond_rm_tmp file = 
-    if !keep_atp_input then Output.debug "ATP input kept..." 
-    else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir))
-    else (Output.debug "deleting ATP inputs..."; OS.FileSys.remove file);
+    if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..." 
+    else OS.FileSys.remove file;
 
 
 (****** setup ATPs as Isabelle methods ******)
 fun atp_meth' tac ths ctxt = 
     Method.SIMPLE_METHOD' HEADGOAL

 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
             let val fname = probfile k
                 val axcls = make_unique axcls
                 val ccls = subtract_cls ccls axcls
                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
-            in  (clnames,fname) :: write_all ccls_list axcls_list (k+1)  end
-      val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
-      val thm_names = Array.fromList clnames
-      val _ = if !Output.show_debug_msgs 
-              then trace_array "thm_names" thm_names else ()
+                val thm_names = Array.fromList clnames
+                val _ = if !Output.show_debug_msgs 
+                        then trace_array (fname ^ "_thm_names") thm_names else ()
+            in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
+      val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   in
-      (filenames, thm_names)
+      (filenames, thm_names_list)
   end;
 
 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
                                     Posix.Process.pid * string list) option);
 

     (case !last_watcher_pid of 
          NONE => ()
        | SOME (_, _, pid, files) => 
 	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
 	   Watcher.killWatcher pid;  
-	   ignore (map (try OS.FileSys.remove) files)))
+	   ignore (map (try cond_rm_tmp) files)))
      handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
 
 (*writes out the current clasimpset to a tptp file;
   turns off xsymbol at start of function, restoring it at end    *)
 val isar_atp = setmp print_mode [] 
  (fn (ctxt, th) =>
   if Thm.no_prems th then ()
   else
     let
       val _ = kill_last_watcher()
-      val (files,thm_names) = write_problem_files prob_pathname (ctxt,th)
-      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
+      val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th)
+      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list)
     in
       last_watcher_pid := SOME (childin, childout, pid, files);
       Output.debug ("problem files: " ^ space_implode ", " files); 
       Output.debug ("pid: " ^ string_of_pid pid);
       watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)