src/Pure/Isar/context_rules.ML
changeset 23227 96f86d377dd9
parent 23178 07ba6b58b3d2
child 25979 3297781f8141
     1.1 --- a/src/Pure/Isar/context_rules.ML	Sun Jun 03 23:16:54 2007 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Jun 03 23:16:55 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 (insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
     1.8 +      (nth_map i (Tactic.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 = Tactic.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,9 +107,9 @@
    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 (insert_tagged_brl ((w, n), (b, th))))
    1.24 +          nth_map i (Tactic.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 +    in make_rules (next - 1) rules netpairs wrappers end;
    1.28  );
    1.29  
    1.30  fun print_rules ctxt =