--- 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);