# HG changeset patch
# User wenzelm
# Date 1236283619 -3600
# Node ID a1c3abf57068e8243b66896a8fad26ac81c9191b
# Parent  f49d70426690303d226141b3383bc1854587c7e6
removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;

diff -r f49d70426690 -r a1c3abf57068 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Mar 05 20:55:28 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML	Thu Mar 05 21:06:59 2009 +0100
@@ -34,8 +34,6 @@
 val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
 val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
 val include_all = true;
-val include_simpset = false;
-val include_claset = false;
 val include_atpset = true;
   
 (***************************************************************)
@@ -409,17 +407,11 @@
                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
                   (name_thm_pairs ctxt))
         else
-        let val claset_thms =
-                if include_claset then ResAxioms.claset_rules_of ctxt
-                else []
-            val simpset_thms =
-                if include_simpset then ResAxioms.simpset_rules_of ctxt
-                else []
-            val atpset_thms =
+        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  claset_thms @ simpset_thms @ atpset_thms  end
+        in  atpset_thms  end
       val user_rules = filter check_named
                          (map ResAxioms.pairname
                            (if null user_thms then whitelist else user_thms))
diff -r f49d70426690 -r a1c3abf57068 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Mar 05 20:55:28 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 05 21:06:59 2009 +0100
@@ -15,8 +15,6 @@
   val expand_defs_tac: thm -> tactic
   val combinators: thm -> thm
   val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
-  val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
-  val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
   val atpset_rules_of: Proof.context -> (string * thm) list
   val suppress_endtheory: bool ref     (*for emergency use where endtheory causes problems*)
   val setup: theory -> theory
@@ -378,24 +376,10 @@
   end;
 
 
-(**** Extract and Clausify theorems from a theory's claset and simpset ****)
+(**** Rules from the context ****)
 
 fun pairname th = (Thm.get_name_hint th, th);
 
-fun rules_of_claset cs =
-  let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
-      val intros = safeIs @ hazIs
-      val elims  = map Classical.classical_rule (safeEs @ hazEs)
-  in map pairname (intros @ elims) end;
-
-fun rules_of_simpset ss =
-  let val ({rules,...}, _) = rep_ss ss
-      val simps = Net.entries rules
-  in map (fn r => (#name r, #thm r)) simps end;
-
-fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
-fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
-
 fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt);