# HG changeset patch
# User wenzelm
# Date 1752262582 -7200
# Node ID 0a8977dcb21a5e69177a09bb68523ec52f71083d
# Parent  d8ecaff223ff9b48ebfd72de2b986918531b1344
more accurate delete operation via authentic index --- minor performance tuning;

diff -r d8ecaff223ff -r 0a8977dcb21a src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Jul 11 15:17:42 2025 +0200
+++ b/src/Provers/classical.ML	Fri Jul 11 21:36:22 2025 +0200
@@ -266,15 +266,15 @@
   insert_brl (2 * k + 1) (Bires.kind_rule kind th) #>
   (case swapped of NONE => I | SOME th' => insert_brl (2 * k) (true, th'));
 
-fun delete_rl kind ((th, swapped): rl) =
-  Bires.delete_tagged_rule (Bires.kind_rule kind th) #>
-  (case swapped of NONE => I | SOME th' => Bires.delete_tagged_rule (true, th'));
+fun delete_rl k ((th, swapped): rl) =
+  Bires.delete_tagged_rule (2 * k + 1, th) #>
+  (case swapped of NONE => I | SOME th' => Bires.delete_tagged_rule (2 * k, th'));
 
 fun insert_plain_rule ({kind, tag, info = {rl = (th, _), ...}}: decl) =
   Bires.insert_tagged_rule (tag, (Bires.kind_elim kind, th));
 
-fun delete_plain_rule ({kind, info = {rl = (th, _), ...}, ...}: decl) =
-  Bires.delete_tagged_rule (Bires.kind_rule kind th);
+fun delete_plain_rule ({tag = {index, ...}, info = {rl = (th, _), ...}, ...}: decl) =
+  Bires.delete_tagged_rule (index, th);
 
 fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
 
@@ -452,7 +452,7 @@
     if null old_decls then (warn_thm ctxt (fn () => "Undeclared classical rule\n") th; cs)
     else
       let
-        fun del which ({kind, info, ...}: decl) = delete_rl kind (which info);
+        fun del which ({tag = {index, ...}, info, ...}: decl) = delete_rl index (which info);
         val safe0_netpair' = fold (del #rl) old_decls safe0_netpair;
         val safep_netpair' = fold (del #rl) old_decls safep_netpair;
         val unsafe_netpair' = fold (del #rl) old_decls unsafe_netpair;
diff -r d8ecaff223ff -r 0a8977dcb21a src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Fri Jul 11 15:17:42 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Fri Jul 11 21:36:22 2025 +0200
@@ -49,8 +49,8 @@
 fun insert_decl ({kind, tag, info = th}: decl) =
   Bires.insert_tagged_rule (tag, Bires.kind_rule kind th);
 
-fun remove_decl ({info = th, ...}: decl) =
-  Bires.delete_tagged_rule (false, th) o Bires.delete_tagged_rule (true, th);
+fun remove_decl ({tag = {index, ...}, info = th, ...}: decl) =
+  Bires.delete_tagged_rule (index, th);
 
 
 (* context data *)
diff -r d8ecaff223ff -r 0a8977dcb21a src/Pure/bires.ML
--- a/src/Pure/bires.ML	Fri Jul 11 15:17:42 2025 +0200
+++ b/src/Pure/bires.ML	Fri Jul 11 21:36:22 2025 +0200
@@ -54,7 +54,7 @@
   type netpair = (tag * rule) Net.net * (tag * rule) Net.net
   val empty_netpair: netpair
   val insert_tagged_rule: tag * rule -> netpair -> netpair
-  val delete_tagged_rule: rule -> netpair -> netpair
+  val delete_tagged_rule: int * thm -> netpair -> netpair
 
   val biresolution_from_nets_tac: Proof.context -> tag ord -> (rule -> bool) option ->
     bool -> netpair -> int -> tactic
@@ -229,19 +229,15 @@
     | NONE => error "insert_tagged_rule: elimination rule with no premises")
   else (Net.insert_term (K false) (Thm.concl_of th, tagged_rule) inet, enet);
 
-local
-  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
-in
-
-fun delete_tagged_rule (brl as (eres, th)) ((inet, enet): netpair) =
-  (if eres then
-    (case try Thm.major_prem_of th of
-      SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
-    | NONE => (inet, enet))  (*no major premise: ignore*)
-  else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
-  handle Net.DELETE => (inet,enet);
-
-end;
+fun delete_tagged_rule (index, th) ((inet, enet): netpair) =
+  let
+    fun eq ((), ({index = index', ...}, _)) = index = index';
+    val inet' = Net.delete_term_safe eq (Thm.concl_of th, ()) inet;
+    val enet' =
+      (case try Thm.major_prem_of th of
+        SOME prem => Net.delete_term_safe eq (prem, ()) enet
+      | NONE => enet);
+  in (inet', enet') end;
 
 
 (*biresolution using a pair of nets rather than rules: