src/HOL/Tools/ATP/res_clasimpset.ML
changeset 19320 d3688974a063
parent 19317 3d383e78b6f4
child 19356 794802e95d35
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Mar 22 18:09:35 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Mar 23 06:18:38 2006 +0100
     1.3 @@ -267,10 +267,10 @@
     1.4        if mem_tm tm tms_names' then insert_tms tms_names tms_names' 
     1.5        else insert_tms tms_names ((tm,name)::tms_names');
     1.6  
     1.7 -fun warning_thms [] = ()
     1.8 -  | warning_thms ((name,thm)::nthms) = 
     1.9 +fun display_thms [] = ()
    1.10 +  | display_thms ((name,thm)::nthms) = 
    1.11        let val nthm = name ^ ": " ^ (string_of_thm thm)
    1.12 -      in warning nthm; warning_thms nthms  end;
    1.13 +      in Output.debug nthm; display_thms nthms  end;
    1.14   
    1.15  (*Write out the claset, simpset and atpset rules of the supplied theory.*)
    1.16  (* also write supplied user rules, they are not relevance filtered *)
    1.17 @@ -287,7 +287,7 @@
    1.18  	  if use_atpset then
    1.19  	      map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt)
    1.20  	  else []
    1.21 -      val _ = warning_thms atpset_thms
    1.22 +      val _ = if !Output.show_debug_msgs then (Output.debug "ATP theorems: "; display_thms atpset_thms) else ()
    1.23        val user_rules = 
    1.24  	  case user_thms of  (*use whitelist if there are no user-supplied rules*)
    1.25  	       [] => map (put_name_pair o ResAxioms.pairname) (!whitelist)