src/Provers/classical.ML

   val del_context_unsafe_wrapper: string -> theory -> theory
   val get_claset: theory -> claset
   val get_local_claset: Proof.context -> claset
   val put_local_claset: claset -> Proof.context -> Proof.context
   val print_local_claset: Proof.context -> unit
+  val get_cs: Context.generic -> claset
+  val map_cs: (claset -> claset) -> Context.generic -> Context.generic
   val safe_dest: int option -> attribute
   val safe_elim: int option -> attribute
   val safe_intro: int option -> attribute
   val haz_dest: int option -> attribute
   val haz_elim: int option -> attribute

 
 
 
 (** claset data **)
 
-(* global claset *)
+(* global clasets *)
 
 structure GlobalClaset = TheoryDataFun
 (
   type T = claset ref * context_cs;
   val empty = (ref empty_cs, empty_context_cs);

   (AList.update (op =) wrapper);
 fun del_context_unsafe_wrapper name = (map_context_cs o apsnd)
   (AList.delete (op =) name);
 
 
-(* local claset *)
+(* local clasets *)
 
 structure LocalClaset = ProofDataFun
 (
   type T = claset;
   val init = get_claset;

 
 fun local_claset_of ctxt =
   context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
 
 val print_local_claset = print_cs o local_claset_of;
+
+
+(* generic clasets *)
+
+fun get_cs (Context.Theory thy) = claset_of thy
+  | get_cs (Context.Proof ctxt) = local_claset_of ctxt;
+
+fun map_cs f (Context.Theory thy) = (change_claset_of thy f; Context.Theory thy)
+  | map_cs f (Context.Proof ctxt) = Context.Proof (LocalClaset.map f ctxt);
 
 
 (* attributes *)
 
 fun attrib f = Thm.declaration_attribute (fn th =>