# HG changeset patch
# User wenzelm
# Date 1751720606 -7200
# Node ID be34513a58a10e5860ec5fe038372a64dba4d115
# Parent  7189368734cdbb8f09bf87a4ebe73d8fb63ffa0f
clarified signature;

diff -r 7189368734cd -r be34513a58a1 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Jul 05 14:39:24 2025 +0200
+++ b/src/Provers/classical.ML	Sat Jul 05 15:03:26 2025 +0200
@@ -273,16 +273,13 @@
 fun tag_brls' _ _ [] = []
   | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
 
-fun insert_tagged_list rls = fold_rev Bires.insert_tagged_brl rls;
-
 (*Insert into netpair that already has nI intr rules and nE elim rules.
   Count the intr rules double (to account for swapify).  Negate to give the
   new insertions the lowest priority.*)
-fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
-fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules;
+fun insert (nI, nE) = Bires.insert_tagged_rules o (tag_brls (~(2*nI+nE))) o joinrules;
+fun insert' w (nI, nE) = Bires.insert_tagged_rules o tag_brls' w (~(nI + nE)) o joinrules;
 
-fun delete_tagged_list rls = fold_rev Bires.delete_tagged_brl rls;
-fun delete x = delete_tagged_list (joinrules x);
+fun delete x = Bires.delete_tagged_rules (joinrules x);
 
 fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
 
diff -r 7189368734cd -r be34513a58a1 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sat Jul 05 14:39:24 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sat Jul 05 15:03:26 2025 +0200
@@ -81,13 +81,13 @@
     val th' = Thm.trim_context th;
   in
     make_rules (next - 1) ((w, ((i, b), th')) :: rules)
-      (nth_map i (Bires.insert_tagged_brl ((w, next), (b, th'))) netpairs) wrappers
+      (nth_map i (Bires.insert_tagged_rule ((w, next), (b, th'))) netpairs) wrappers
   end;
 
 fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
   let
     fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
-    fun del b netpair = Bires.delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
+    fun del b netpair = Bires.delete_tagged_rule (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
@@ -109,7 +109,7 @@
           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 (Bires.insert_tagged_brl ((w, n), (b, th))))
+          nth_map i (Bires.insert_tagged_rule ((w, n), (b, th))))
         (next upto ~1 ~~ rules) empty_netpairs;
     in make_rules (next - 1) rules netpairs wrappers end;
 );
diff -r 7189368734cd -r be34513a58a1 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Sat Jul 05 14:39:24 2025 +0200
+++ b/src/Pure/bires.ML	Sat Jul 05 15:03:26 2025 +0200
@@ -9,8 +9,10 @@
 sig
   type rule = bool * thm
   type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net;
-  val insert_tagged_brl: 'a * rule -> 'a netpair -> 'a netpair
-  val delete_tagged_brl: rule -> 'a netpair -> 'a netpair
+  val insert_tagged_rule: 'a * rule -> 'a netpair -> 'a netpair
+  val insert_tagged_rules: ('a * rule) list -> 'a netpair -> 'a netpair
+  val delete_tagged_rule: rule -> 'a netpair -> 'a netpair
+  val delete_tagged_rules: rule list -> 'a netpair -> 'a netpair
   val eq_kbrl: ('a * rule) * ('a * rule) -> bool
   val build_net: thm list -> (int * thm) Net.net
   val biresolution_from_nets_tac: Proof.context ->
@@ -33,17 +35,20 @@
 (** To preserve the order of the rules, tag them with increasing integers **)
 
 (*insert one tagged brl into the pair of nets*)
-fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
+fun insert_tagged_rule (kbrl as (k, (eres, th))) (inet, enet) =
   if eres then
     (case try Thm.major_prem_of th of
       SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
-    | NONE => error "insert_tagged_brl: elimination rule with no premises")
+    | NONE => error "insert_tagged_rule: elimination rule with no premises")
   else (Net.insert_term (K false) (Thm.concl_of th, kbrl) inet, enet);
 
+fun insert_tagged_rules rls = fold_rev insert_tagged_rule rls;
+
+
 (*delete one kbrl from the pair of nets*)
 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
 
-fun delete_tagged_brl (brl as (eres, th)) (inet, enet) =
+fun delete_tagged_rule (brl as (eres, th)) (inet, enet) =
   (if eres then
     (case try Thm.major_prem_of th of
       SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
@@ -51,6 +56,8 @@
   else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
   handle Net.DELETE => (inet,enet);
 
+fun delete_tagged_rules rls = fold_rev delete_tagged_rule rls;
+
 
 (*biresolution using a pair of nets rather than rules.
     function "order" must sort and possibly filter the list of brls.