tuned;
authorwenzelm
Fri, 11 Jul 2025 21:38:14 +0200
changeset 82849 42b584d92673
parent 82848 0a8977dcb21a
child 82850 3020b1660bec
tuned;
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;