# HG changeset patch
# User wenzelm
# Date 1752575870 -7200
# Node ID 9cdc0504aa2f3b25fce466e81dbcab5004823701
# Parent  abfb6ed8ec21454ae2016c7534502e891176dd28
clarified messages;

diff -r abfb6ed8ec21 -r 9cdc0504aa2f src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jul 15 11:56:24 2025 +0200
+++ b/src/Provers/classical.ML	Tue Jul 15 12:37:50 2025 +0200
@@ -433,6 +433,11 @@
     val CS {decls, swrappers, uwrappers,
       safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair} = cs;
     val (old_decls, decls') = Bires.remove_decls th decls;
+    val _ =
+      if Bires.has_decls decls (Tactic.make_elim th) then
+        warn_thm ctxt
+          (fn () => "Not deleting elim format --- need to to declare proper dest rule\n") th
+      else ();
   in
     if null old_decls then
       (if warn then warn_thm ctxt (fn () => "Undeclared classical rule\n") th else (); cs)