author | wenzelm |
Fri, 11 Jul 2025 21:39:03 +0200 | |
changeset 82850 | 3020b1660bec |
parent 82849 | 42b584d92673 |
child 82851 | 7f9c4466c6a5 |
--- 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 (