clarified messages;
authorwenzelm
Tue, 15 Jul 2025 12:37:50 +0200
changeset 82875 9cdc0504aa2f
parent 82874 abfb6ed8ec21
child 82876 9a19d83dfd5c
clarified messages;
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)