1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 06 11:17:53 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 06 15:38:29 2006 +0200
     1.3 @@ -30,7 +30,6 @@
     1.4    val atp_method: (Proof.context -> thm list -> int -> tactic) ->
     1.5      Method.src -> Proof.context -> Proof.method
     1.6    val cond_rm_tmp: string -> unit
     1.7 -  val keep_atp_input: bool ref
     1.8    val fol_keep_types: bool ref
     1.9    val hol_full_types: unit -> unit
    1.10    val hol_partial_types: unit -> unit
    1.11 @@ -113,7 +112,6 @@
    1.12  fun eproverLimit () = !eprover_time;
    1.13  fun spassLimit () = !spass_time;
    1.14  
    1.15 -val keep_atp_input = ref false;
    1.16  val fol_keep_types = ResClause.keep_types;
    1.17  val hol_full_types = ResHolClause.full_types;
    1.18  val hol_partial_types = ResHolClause.partial_types;
    1.19 @@ -690,9 +688,8 @@
    1.20  
    1.21  (**** remove tmp files ****)
    1.22  fun cond_rm_tmp file = 
    1.23 -    if !keep_atp_input then Output.debug "ATP input kept..." 
    1.24 -    else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir))
    1.25 -    else (Output.debug "deleting ATP inputs..."; OS.FileSys.remove file);
    1.26 +    if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..." 
    1.27 +    else OS.FileSys.remove file;
    1.28  
    1.29  
    1.30  (****** setup ATPs as Isabelle methods ******)
    1.31 @@ -809,13 +806,13 @@
    1.32                  val axcls = make_unique axcls
    1.33                  val ccls = subtract_cls ccls axcls
    1.34                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    1.35 -            in  (clnames,fname) :: write_all ccls_list axcls_list (k+1)  end
    1.36 -      val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
    1.37 -      val thm_names = Array.fromList clnames
    1.38 -      val _ = if !Output.show_debug_msgs 
    1.39 -              then trace_array "thm_names" thm_names else ()
    1.40 +                val thm_names = Array.fromList clnames
    1.41 +                val _ = if !Output.show_debug_msgs 
    1.42 +                        then trace_array (fname ^ "_thm_names") thm_names else ()
    1.43 +            in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
    1.44 +      val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
    1.45    in
    1.46 -      (filenames, thm_names)
    1.47 +      (filenames, thm_names_list)
    1.48    end;
    1.49  
    1.50  val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
    1.51 @@ -827,7 +824,7 @@
    1.52         | SOME (_, _, pid, files) => 
    1.53  	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
    1.54  	   Watcher.killWatcher pid;  
    1.55 -	   ignore (map (try OS.FileSys.remove) files)))
    1.56 +	   ignore (map (try cond_rm_tmp) files)))
    1.57       handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
    1.58  
    1.59  (*writes out the current clasimpset to a tptp file;
    1.60 @@ -838,8 +835,8 @@
    1.61    else
    1.62      let
    1.63        val _ = kill_last_watcher()
    1.64 -      val (files,thm_names) = write_problem_files prob_pathname (ctxt,th)
    1.65 -      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
    1.66 +      val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th)
    1.67 +      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list)
    1.68      in
    1.69        last_watcher_pid := SOME (childin, childout, pid, files);
    1.70        Output.debug ("problem files: " ^ space_implode ", " files);