Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
redundant: Net.DELETE already handled;
authorwenzelm
Wed, 09 Jul 2025 17:00:03 +0200
changeset 82835 6d1914817496
parent 82834 0b2acd437db4
child 82836 68a0219861b7
redundant: Net.DELETE already handled;
src/Pure/bires.ML file | annotate | diff | comparison | revisions 
--- 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:
isabelle