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