# HG changeset patch
# User wenzelm
# Date 1752073179 -7200
# Node ID 0b2acd437db44f765b16eb1ba4edaa8b0ef382ea
# Parent  13a8c49a48a06d138b3c95844ae60cce0a187dda
tuned;

diff -r 13a8c49a48a0 -r 0b2acd437db4 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Wed Jul 09 12:48:44 2025 +0200
+++ b/src/FOLP/simp.ML	Wed Jul 09 16:59:39 2025 +0200
@@ -267,10 +267,8 @@
 
 (** Deletion of congruences and rewrites **)
 
-(*delete a thm from a thm net*)
 fun delete_thm th net =
-  Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net
-    handle Net.DELETE => net;
+  Net.delete_term_safe Thm.eq_thm_prop (Thm.concl_of th, th) net;
 
 val delete_thms = fold_rev delete_thm;