# HG changeset patch
# User wenzelm
# Date 1752227962 -7200
# Node ID c3085510366ea11a6ed3f00cacb5616b8e129fd2
# Parent  60ec2b2dc55a58dcd1cfed70c22361659531784c
clarified modules;

diff -r 60ec2b2dc55a -r c3085510366e src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Jul 11 11:52:43 2025 +0200
+++ b/src/Provers/classical.ML	Fri Jul 11 11:59:22 2025 +0200
@@ -287,12 +287,12 @@
 
 (*Insert into netpair from next index, which is negative to give the
   new insertions the lowest priority.*)
-fun insert k = Bires.insert_tagged_rules o (tag_brls (2 * k)) o joinrules;
+fun insert k = fold_rev Bires.insert_tagged_rule o (tag_brls (2 * k)) o joinrules;
 
 fun insert_default_weight w0 w k =
-  Bires.insert_tagged_rules o tag_weight_brls (the_default w0 w) k o single;
+  fold_rev Bires.insert_tagged_rule o tag_weight_brls (the_default w0 w) k o single;
 
-fun delete x = Bires.delete_tagged_rules (joinrules x);
+fun delete x = fold_rev Bires.delete_tagged_rule (joinrules x);
 
 fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
 
diff -r 60ec2b2dc55a -r c3085510366e src/Pure/bires.ML
--- a/src/Pure/bires.ML	Fri Jul 11 11:52:43 2025 +0200
+++ b/src/Pure/bires.ML	Fri Jul 11 11:59:22 2025 +0200
@@ -50,9 +50,7 @@
   type netpair = (tag * rule) Net.net * (tag * rule) Net.net
   val empty_netpair: netpair
   val insert_tagged_rule: tag * rule -> netpair -> netpair
-  val insert_tagged_rules: (tag * rule) list -> netpair -> netpair
   val delete_tagged_rule: rule -> netpair -> netpair
-  val delete_tagged_rules: rule list -> netpair -> netpair
 
   val biresolution_from_nets_tac: Proof.context -> tag ord -> (rule -> bool) option ->
     bool -> netpair -> int -> tactic
@@ -223,9 +221,6 @@
     | NONE => error "insert_tagged_rule: elimination rule with no premises")
   else (Net.insert_term (K false) (Thm.concl_of th, tagged_rule) inet, enet);
 
-fun insert_tagged_rules rls = fold_rev insert_tagged_rule rls;
-
-
 local
   fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
 in
@@ -240,8 +235,6 @@
 
 end;
 
-fun delete_tagged_rules rls = fold_rev delete_tagged_rule rls;
-
 
 (*biresolution using a pair of nets rather than rules:
    boolean "match" indicates matching or unification.*)