more robust: no failure on bad rule;
authorwenzelm
Fri, 11 Jul 2025 21:39:03 +0200
changeset 82850 3020b1660bec
parent 82849 42b584d92673
child 82851 7f9c4466c6a5
more robust: no failure on bad rule;
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
 (