src/Pure/Isar/context_rules.ML
changeset 45375 7fe19930dfc9
parent 39557 fe5722fce758
child 51580 64ef8260dc60
     1.1 --- a/src/Pure/Isar/context_rules.ML	Sun Nov 06 21:17:45 2011 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Nov 06 21:51:46 2011 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4        (nth_map i (Tactic.insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
     1.5    end;
     1.6  
     1.7 -fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
     1.8 +fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
     1.9    let
    1.10      fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
    1.11      fun del b netpair = Tactic.delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
    1.12 @@ -89,6 +89,8 @@
    1.13      else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
    1.14    end;
    1.15  
    1.16 +fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th);
    1.17 +
    1.18  structure Rules = Generic_Data
    1.19  (
    1.20    type T = rules;
    1.21 @@ -179,11 +181,11 @@
    1.22  
    1.23  (* add and del rules *)
    1.24  
    1.25 -fun rule_del (x, th) =
    1.26 -  (Rules.map (del_rule th o del_rule (Tactic.make_elim th)) x, th);
    1.27 +
    1.28 +val rule_del = Thm.declaration_attribute (fn th => Rules.map (del_rule th));
    1.29  
    1.30  fun rule_add k view opt_w =
    1.31 -  (fn (x, th) => (Rules.map (add_rule k opt_w (view th)) x, th)) o rule_del;
    1.32 +  Thm.declaration_attribute (fn th => Rules.map (add_rule k opt_w (view th) o del_rule th));
    1.33  
    1.34  val intro_bang  = rule_add intro_bangK I;
    1.35  val elim_bang   = rule_add elim_bangK I;