--- 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);
--- 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.*)