# HG changeset patch
# User wenzelm
# Date 1752262694 -7200
# Node ID 42b584d926733f5cc8055604a5bfa610b923be5a
# Parent  0a8977dcb21a5e69177a09bb68523ec52f71083d
tuned;

diff -r 0a8977dcb21a -r 42b584d92673 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Jul 11 21:36:22 2025 +0200
+++ b/src/Provers/classical.ML	Fri Jul 11 21:38:14 2025 +0200
@@ -444,7 +444,7 @@
 
 fun delrule ctxt th cs =
   let
-    val ths = th :: ([Tactic.make_elim th] handle THM _ => []);
+    val ths = th :: the_list (try Tactic.make_elim th);
     val CS {decls, swrappers, uwrappers,
       safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair} = cs;
     val (old_decls, decls') = fold_map Bires.remove_decls ths decls |>> flat;