src/Pure/Isar/context_rules.ML
changeset 23178 07ba6b58b3d2
parent 22846 fb79144af9a3
child 23227 96f86d377dd9
     1.1 --- a/src/Pure/Isar/context_rules.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -80,13 +80,13 @@
     1.4  fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
     1.5    let val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)) in
     1.6      make_rules (next - 1) ((w, ((i, b), th)) :: rules)
     1.7 -      (nth_map i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
     1.8 +      (nth_map i (insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
     1.9    end;
    1.10  
    1.11  fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
    1.12    let
    1.13      fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
    1.14 -    fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
    1.15 +    fun del b netpair = delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
    1.16    in
    1.17      if not (exists eq_th rules) then rs
    1.18      else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
    1.19 @@ -107,7 +107,7 @@
    1.20            k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
    1.21        val next = ~ (length rules);
    1.22        val netpairs = fold (fn (n, (w, ((i, b), th))) =>
    1.23 -          nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
    1.24 +          nth_map i (insert_tagged_brl ((w, n), (b, th))))
    1.25          (next upto ~1 ~~ rules) empty_netpairs;
    1.26      in make_rules (next - 1) rules netpairs wrappers end
    1.27  );