# HG changeset patch
# User paulson
# Date 1246528186 -3600
# Node ID a8e9ccfc427a26d3dd4070d711355d98ebab4225
# Parent  d3b020134006e2a3191fd53a5902223b4d4d9134
Deleted some debugging code

diff -r d3b020134006 -r a8e9ccfc427a src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Jul 01 16:19:44 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML	Thu Jul 02 10:49:46 2009 +0100
@@ -219,8 +219,7 @@
 	    handle ConstFree => false
     in    
 	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
-		   defs lhs rhs andalso
-		   (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
+		   defs lhs rhs 
 		 | _ => false
     end;
 
@@ -276,8 +275,7 @@
 fun relevance_filter max_new theory_const thy axioms goals = 
  if run_relevance_filter andalso pass_mark >= 0.1
  then
-  let val _ = Output.debug (fn () => "Start of relevance filtering");
-      val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
+  let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
       val goal_const_tab = get_goal_consts_typs thy goals
       val _ = Output.debug (fn () => ("Initial constants: " ^
                                  space_implode ", " (Symtab.keys goal_const_tab)));
@@ -406,8 +404,6 @@
 fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
   | check_named (_,th) = true;
 
-fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th);
-
 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
 fun get_clasimp_atp_lemmas ctxt =
   let val included_thms =
@@ -419,7 +415,6 @@
     let val atpset_thms =
             if include_atpset then ResAxioms.atpset_rules_of ctxt
             else []
-        val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
     in  atpset_thms  end
   in
     filter check_named included_thms
diff -r d3b020134006 -r a8e9ccfc427a src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Jul 01 16:19:44 2009 +0100
+++ b/src/HOL/Tools/res_clause.ML	Thu Jul 02 10:49:46 2009 +0100
@@ -381,8 +381,6 @@
   | iter_type_class_pairs thy tycons classes =
       let val cpairs = type_class_pairs thy tycons classes
           val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
-          val _ = if null newclasses then ()
-                  else Output.debug (fn _ => "New classes: " ^ space_implode ", " newclasses)
           val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
       in  (classes' union classes, cpairs' union cpairs)  end;
 
diff -r d3b020134006 -r a8e9ccfc427a src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Wed Jul 01 16:19:44 2009 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jul 02 10:49:46 2009 +0100
@@ -419,13 +419,13 @@
         val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
         fun needed c = valOf (Symtab.lookup ct c) > 0
         val IK = if needed "c_COMBI" orelse needed "c_COMBK"
-                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
+                 then cnf_helper_thms thy [comb_I,comb_K]
                  else []
         val BC = if needed "c_COMBB" orelse needed "c_COMBC"
-                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C])
+                 then cnf_helper_thms thy [comb_B,comb_C]
                  else []
         val S = if needed "c_COMBS"
-                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
+                then cnf_helper_thms thy [comb_S]
                 else []
         val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
     in