# HG changeset patch
# User wenzelm
# Date 1180905415 -7200
# Node ID 96f86d377dd99ef2d681bf82215bf7c7a0dc5d01
# Parent  441f8a0bd766c54258ba3354fa590a4f4a1f2e15
tuned Tactic signature;

diff -r 441f8a0bd766 -r 96f86d377dd9 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sun Jun 03 23:16:54 2007 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sun Jun 03 23:16:55 2007 +0200
@@ -80,13 +80,13 @@
 fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
   let val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)) in
     make_rules (next - 1) ((w, ((i, b), th)) :: rules)
-      (nth_map i (insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
+      (nth_map i (Tactic.insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
   end;
 
 fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
   let
     fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
-    fun del b netpair = delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
+    fun del b netpair = Tactic.delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
   in
     if not (exists eq_th rules) then rs
     else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
@@ -107,9 +107,9 @@
           k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
       val next = ~ (length rules);
       val netpairs = fold (fn (n, (w, ((i, b), th))) =>
-          nth_map i (insert_tagged_brl ((w, n), (b, th))))
+          nth_map i (Tactic.insert_tagged_brl ((w, n), (b, th))))
         (next upto ~1 ~~ rules) empty_netpairs;
-    in make_rules (next - 1) rules netpairs wrappers end
+    in make_rules (next - 1) rules netpairs wrappers end;
 );
 
 fun print_rules ctxt =