diff -r e4ad74159b43 -r 9b883c416aef src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Mon Sep 04 21:18:33 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Sep 04 21:19:07 2000 +0200
@@ -109,8 +109,8 @@
 
 (** monotonicity rules **)
 
-val get_monos = snd o InductiveData.get;
-fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
+val get_monos = #2 o InductiveData.get;
+fun map_monos f = InductiveData.map (Library.apsnd f);
 
 fun mk_mono thm =
   let
@@ -130,19 +130,8 @@
 
 (* attributes *)
 
-local
-
-fun map_rules_global f thy = put_monos (f (get_monos thy)) thy;
-
-fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules);
-fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm);
-
-fun mk_att f g (x, thm) = (f (g thm) x, thm);
-
-in
-  val mono_add_global = mk_att map_rules_global add_mono;
-  val mono_del_global = mk_att map_rules_global del_mono;
-end;
+fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
+fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
 
 val mono_attr =
  (Attrib.add_del_args mono_add_global mono_del_global,