diff -r 7e1f85ceb1a2 -r d3688974a063 src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Mar 22 18:09:35 2006 +0100
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Mar 23 06:18:38 2006 +0100
@@ -267,10 +267,10 @@
       if mem_tm tm tms_names' then insert_tms tms_names tms_names' 
       else insert_tms tms_names ((tm,name)::tms_names');
 
-fun warning_thms [] = ()
-  | warning_thms ((name,thm)::nthms) = 
+fun display_thms [] = ()
+  | display_thms ((name,thm)::nthms) = 
       let val nthm = name ^ ": " ^ (string_of_thm thm)
-      in warning nthm; warning_thms nthms  end;
+      in Output.debug nthm; display_thms nthms  end;
  
 (*Write out the claset, simpset and atpset rules of the supplied theory.*)
 (* also write supplied user rules, they are not relevance filtered *)
@@ -287,7 +287,7 @@
 	  if use_atpset then
 	      map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt)
 	  else []
-      val _ = warning_thms atpset_thms
+      val _ = if !Output.show_debug_msgs then (Output.debug "ATP theorems: "; display_thms atpset_thms) else ()
       val user_rules = 
 	  case user_thms of  (*use whitelist if there are no user-supplied rules*)
 	       [] => map (put_name_pair o ResAxioms.pairname) (!whitelist)