src/Pure/simplifier.ML

   val clear_ss: simpset -> simpset
   val debug_bounds: bool Unsynchronized.ref
   val prems_of: simpset -> thm list
   val add_simp: thm -> simpset -> simpset
   val del_simp: thm -> simpset -> simpset
+  val add_eqcong: thm -> simpset -> simpset
+  val del_eqcong: thm -> simpset -> simpset
+  val add_cong: thm -> simpset -> simpset
+  val del_cong: thm -> simpset -> simpset
   val add_prems: thm list -> simpset -> simpset
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
   val global_context: theory -> simpset -> simpset

   val full_rewrite: simpset -> conv
   val asm_lr_rewrite: simpset -> conv
   val asm_full_rewrite: simpset -> conv
   val get_ss: Context.generic -> simpset
   val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
-  val attrib: (simpset * thm list -> simpset) -> attribute
+  val attrib: (thm -> simpset -> simpset) -> attribute
   val simp_add: attribute
   val simp_del: attribute
   val cong_add: attribute
   val cong_del: attribute
   val check_simproc: Proof.context -> xstring * Position.T -> string

 
 (** simpset data **)
 
 (* attributes *)
 
-fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
-
-val simp_add = attrib (op addsimps);
-val simp_del = attrib (op delsimps);
-val cong_add = attrib (op addcongs);
-val cong_del = attrib (op delcongs);
+fun attrib f = Thm.declaration_attribute (map_ss o f);
+
+val simp_add = attrib add_simp;
+val simp_del = attrib del_simp;
+val cong_add = attrib add_cong;
+val cong_del = attrib del_cong;
 
 
 (* local simpset *)
 
 fun map_simpset f = Context.proof_map (map_ss f);