src/HOL/Tools/res_axioms.ML
changeset 30291 a1c3abf57068
parent 30280 eb98b49ef835
child 30364 577edc39b501
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Mar 05 20:55:28 2009 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 05 21:06:59 2009 +0100
     1.3 @@ -15,8 +15,6 @@
     1.4    val expand_defs_tac: thm -> tactic
     1.5    val combinators: thm -> thm
     1.6    val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
     1.7 -  val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
     1.8 -  val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
     1.9    val atpset_rules_of: Proof.context -> (string * thm) list
    1.10    val suppress_endtheory: bool ref     (*for emergency use where endtheory causes problems*)
    1.11    val setup: theory -> theory
    1.12 @@ -378,24 +376,10 @@
    1.13    end;
    1.14  
    1.15  
    1.16 -(**** Extract and Clausify theorems from a theory's claset and simpset ****)
    1.17 +(**** Rules from the context ****)
    1.18  
    1.19  fun pairname th = (Thm.get_name_hint th, th);
    1.20  
    1.21 -fun rules_of_claset cs =
    1.22 -  let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
    1.23 -      val intros = safeIs @ hazIs
    1.24 -      val elims  = map Classical.classical_rule (safeEs @ hazEs)
    1.25 -  in map pairname (intros @ elims) end;
    1.26 -
    1.27 -fun rules_of_simpset ss =
    1.28 -  let val ({rules,...}, _) = rep_ss ss
    1.29 -      val simps = Net.entries rules
    1.30 -  in map (fn r => (#name r, #thm r)) simps end;
    1.31 -
    1.32 -fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
    1.33 -fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
    1.34 -
    1.35  fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt);
    1.36  
    1.37