src/HOL/Tools/inductive_package.ML
changeset 9831 9b883c416aef
parent 9804 ee0c337327cf
child 9893 93d2fde0306c
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Sep 04 21:18:33 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Sep 04 21:19:07 2000 +0200
     1.3 @@ -109,8 +109,8 @@
     1.4  
     1.5  (** monotonicity rules **)
     1.6  
     1.7 -val get_monos = snd o InductiveData.get;
     1.8 -fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
     1.9 +val get_monos = #2 o InductiveData.get;
    1.10 +fun map_monos f = InductiveData.map (Library.apsnd f);
    1.11  
    1.12  fun mk_mono thm =
    1.13    let
    1.14 @@ -130,19 +130,8 @@
    1.15  
    1.16  (* attributes *)
    1.17  
    1.18 -local
    1.19 -
    1.20 -fun map_rules_global f thy = put_monos (f (get_monos thy)) thy;
    1.21 -
    1.22 -fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules);
    1.23 -fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm);
    1.24 -
    1.25 -fun mk_att f g (x, thm) = (f (g thm) x, thm);
    1.26 -
    1.27 -in
    1.28 -  val mono_add_global = mk_att map_rules_global add_mono;
    1.29 -  val mono_del_global = mk_att map_rules_global del_mono;
    1.30 -end;
    1.31 +fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
    1.32 +fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
    1.33  
    1.34  val mono_attr =
    1.35   (Attrib.add_del_args mono_add_global mono_del_global,