src/Pure/Isar/spec_rules.ML

 sig
   datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive
   type spec = rough_classification * (term list * thm list)
   val get: Proof.context -> spec list
   val get_global: theory -> spec list
+  val retrieve: Proof.context -> term -> spec list
+  val retrieve_global: theory -> term -> spec list
   val add: rough_classification -> term list * thm list -> local_theory -> local_theory
   val add_global: rough_classification -> term list * thm list -> theory -> theory
 end;
 
 structure Spec_Rules: SPEC_RULES =

 );
 
 val get = Item_Net.content o Rules.get o Context.Proof;
 val get_global = Item_Net.content o Rules.get o Context.Theory;
 
+val retrieve = Item_Net.retrieve o Rules.get o Context.Proof;
+val retrieve_global = Item_Net.retrieve o Rules.get o Context.Theory;
+
 fun add class (ts, ths) lthy =
   let
     val cts = map (Thm.cterm_of (ProofContext.theory_of lthy)) ts;
   in
     lthy |> Local_Theory.declaration true