diff -r 834c4604de7b -r 62753ae847a2 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Fri Jan 26 10:46:15 2007 +0100
+++ b/src/HOL/Tools/res_atp.ML	Fri Jan 26 10:46:22 2007 +0100
@@ -337,6 +337,7 @@
    "Fun.vimage_image_eq",   (*involves an existential quantifier*)
    "HOL.split_if_asm",     (*splitting theorem*)
    "HOL.split_if",         (*splitting theorem*)
+   "HOL.All_def",          (*far worse than useless!!*)
    "IntDef.abs_split",
    "IntDef.Integ.Abs_Integ_inject",
    "IntDef.Integ.Abs_Integ_inverse",
@@ -423,7 +424,7 @@
    "Set.Diff_insert0",
    "Set.empty_Union_conv",   (*redundant with paramodulation*)
    "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
-   "Set.image_Collect",      (*involves an existential quantifier*)
+   "Set.image_Collect",      (*involves Collect and a boolean variable...*)
    "Set.image_def",          (*involves an existential quantifier*)
    "Set.Int_UNIV",  (*redundant with paramodulation*)
    "Set.Inter_iff", (*We already have InterI, InterE*)
@@ -526,11 +527,6 @@
 fun get_relevant_clauses thy cls_thms white_cls goals =
   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
 
-fun display_thms [] = ()
-  | display_thms ((name,thm)::nthms) =
-      let val nthm = name ^ ": " ^ (string_of_thm thm)
-      in Output.debug (fn () => nthm); display_thms nthms  end;
-
 fun all_valid_thms ctxt =
   PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @
   filter (ProofContext.valid_thms ctxt)
@@ -566,6 +562,8 @@
 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   | check_named (_,th) = true;
 
+fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ string_of_thm th);
+
 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
 fun get_clasimp_atp_lemmas ctxt user_thms =
   let val included_thms =
@@ -583,9 +581,7 @@
             val atpset_thms =
                 if !include_atpset then ResAxioms.atpset_rules_of ctxt
                 else []
-            val _ = if !Output.debugging
-                    then (Output.debug (fn () => "ATP theorems: "); display_thms atpset_thms)
-                    else ()
+            val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
         in  claset_thms @ simpset_thms @ atpset_thms  end
       val user_rules = filter check_named
                          (map (ResAxioms.pairname)
@@ -819,8 +815,9 @@
     Output.debug (fn () => "Sent commands to watcher!")
   end
 
+(*For debugging the generated set of theorem names*)
 fun trace_vector fname =
-  let val path = File.explode_platform_path fname
+  let val path = File.explode_platform_path (fname ^ "_thm_names")
   in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
 
 (*We write out problem files for each subgoal. Argument probfile generates filenames,
@@ -868,8 +865,7 @@
                 val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
                 val thm_names = Vector.fromList clnames
-                val _ = if !Output.debugging
-                        then trace_vector (fname ^ "_thm_names") thm_names else ()
+                val _ = if !Output.debugging then trace_vector fname 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
@@ -932,7 +928,8 @@
     ResClause.init thy;
     ResHolClause.init thy;
     if !time_limit > 0 then isar_atp (ctxt, goal)
-    else (warning "Writing problem file only"; isar_atp_writeonly (ctxt, goal))
+    else (warning ("Writing problem file only: " ^ !problem_name); 
+          isar_atp_writeonly (ctxt, goal))
   end;
 
 val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep