Deleted some debugging code
authorpaulson
Thu Jul 02 10:49:46 2009 +0100 (2009-07-02)
changeset 31910a8e9ccfc427a
parent 31909 d3b020134006
child 31911 b8784cb17a35
Deleted some debugging code
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jul 01 16:19:44 2009 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jul 02 10:49:46 2009 +0100
     1.3 @@ -219,8 +219,7 @@
     1.4  	    handle ConstFree => false
     1.5      in    
     1.6  	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
     1.7 -		   defs lhs rhs andalso
     1.8 -		   (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
     1.9 +		   defs lhs rhs 
    1.10  		 | _ => false
    1.11      end;
    1.12  
    1.13 @@ -276,8 +275,7 @@
    1.14  fun relevance_filter max_new theory_const thy axioms goals = 
    1.15   if run_relevance_filter andalso pass_mark >= 0.1
    1.16   then
    1.17 -  let val _ = Output.debug (fn () => "Start of relevance filtering");
    1.18 -      val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
    1.19 +  let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
    1.20        val goal_const_tab = get_goal_consts_typs thy goals
    1.21        val _ = Output.debug (fn () => ("Initial constants: " ^
    1.22                                   space_implode ", " (Symtab.keys goal_const_tab)));
    1.23 @@ -406,8 +404,6 @@
    1.24  fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
    1.25    | check_named (_,th) = true;
    1.26  
    1.27 -fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th);
    1.28 -
    1.29  (* get lemmas from claset, simpset, atpset and extra supplied rules *)
    1.30  fun get_clasimp_atp_lemmas ctxt =
    1.31    let val included_thms =
    1.32 @@ -419,7 +415,6 @@
    1.33      let val atpset_thms =
    1.34              if include_atpset then ResAxioms.atpset_rules_of ctxt
    1.35              else []
    1.36 -        val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
    1.37      in  atpset_thms  end
    1.38    in
    1.39      filter check_named included_thms
     2.1 --- a/src/HOL/Tools/res_clause.ML	Wed Jul 01 16:19:44 2009 +0100
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Jul 02 10:49:46 2009 +0100
     2.3 @@ -381,8 +381,6 @@
     2.4    | iter_type_class_pairs thy tycons classes =
     2.5        let val cpairs = type_class_pairs thy tycons classes
     2.6            val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
     2.7 -          val _ = if null newclasses then ()
     2.8 -                  else Output.debug (fn _ => "New classes: " ^ space_implode ", " newclasses)
     2.9            val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
    2.10        in  (classes' union classes, cpairs' union cpairs)  end;
    2.11  
     3.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Jul 01 16:19:44 2009 +0100
     3.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jul 02 10:49:46 2009 +0100
     3.3 @@ -419,13 +419,13 @@
     3.4          val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
     3.5          fun needed c = valOf (Symtab.lookup ct c) > 0
     3.6          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
     3.7 -                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
     3.8 +                 then cnf_helper_thms thy [comb_I,comb_K]
     3.9                   else []
    3.10          val BC = if needed "c_COMBB" orelse needed "c_COMBC"
    3.11 -                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C])
    3.12 +                 then cnf_helper_thms thy [comb_B,comb_C]
    3.13                   else []
    3.14          val S = if needed "c_COMBS"
    3.15 -                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
    3.16 +                then cnf_helper_thms thy [comb_S]
    3.17                  else []
    3.18          val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
    3.19      in