# HG changeset patch
# User wenzelm
# Date 1752073203 -7200
# Node ID 6d1914817496fdcd92b84ad18a28324e509ff67b
# Parent  0b2acd437db44f765b16eb1ba4edaa8b0ef382ea
redundant: Net.DELETE already handled;

diff -r 0b2acd437db4 -r 6d1914817496 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Wed Jul 09 16:59:39 2025 +0200
+++ b/src/Pure/bires.ML	Wed Jul 09 17:00:03 2025 +0200
@@ -243,8 +243,7 @@
   insert_tagged_rule (tag, kind_rule kind thm) netpair;
 
 fun remove_rule thm =
-  let fun del b netpair = delete_tagged_rule (b, thm) netpair handle Net.DELETE => netpair
-  in del false o del true end;
+  delete_tagged_rule (false, thm) o delete_tagged_rule (true, thm);
 
 
 (*biresolution using a pair of nets rather than rules: