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