# HG changeset patch
# User wenzelm
# Date 1752262743 -7200
# Node ID 3020b1660bec2b8f09254419a018b99748489b65
# Parent  42b584d926733f5cc8055604a5bfa610b923be5a
more robust: no failure on bad rule;

diff -r 42b584d92673 -r 3020b1660bec src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Fri Jul 11 21:38:14 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Fri Jul 11 21:39:03 2025 +0200
@@ -87,7 +87,8 @@
             old_decls netpairs;
       in make_rules decls' netpairs' wrappers end);
 
-fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th);
+fun del_rule th =
+  fold del_rule0 (th :: the_list (try Tactic.make_elim th));
 
 structure Data = Generic_Data
 (