# HG changeset patch
# User wenzelm
# Date 1752573384 -7200
# Node ID abfb6ed8ec21454ae2016c7534502e891176dd28
# Parent  e567fd948ff0803793ed67705ed8ad267fdc1147
more accurate warning;

diff -r e567fd948ff0 -r abfb6ed8ec21 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jul 15 11:26:31 2025 +0200
+++ b/src/Provers/classical.ML	Tue Jul 15 11:56:24 2025 +0200
@@ -428,13 +428,14 @@
 
 (* delete rules *)
 
-fun delrule ctxt th cs =
+fun delrule ctxt warn th cs =
   let
     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;
   in
-    if null old_decls then (warn_thm ctxt (fn () => "Undeclared classical rule\n") th; cs)
+    if null old_decls then
+      (if warn then warn_thm ctxt (fn () => "Undeclared classical rule\n") th else (); cs)
     else
       let
         fun del which ({tag = {index, ...}, info, ...}: decl) = delete_rl index (which info);
@@ -502,7 +503,7 @@
 val op addEs = ml_decl Bires.elim_kind;
 val op addDs = ml_decl Bires.dest_kind;
 
-fun ctxt delrules ths = map_claset (fold_rev (delrule ctxt) ths) ctxt;
+fun ctxt delrules ths = map_claset (fold_rev (delrule ctxt true) ths) ctxt;
 
 
 
@@ -747,7 +748,7 @@
 val rule_del =
   Thm.declaration_attribute (fn th => fn context =>
     context
-    |> map_cs (delrule (Context.proof_of context) th)
+    |> map_cs (delrule (Context.proof_of context) (not (Context_Rules.declared_rule context th)) th)
     |> Thm.attribute_declaration Context_Rules.rule_del th);
 
 
diff -r e567fd948ff0 -r abfb6ed8ec21 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Tue Jul 15 11:26:31 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Tue Jul 15 11:56:24 2025 +0200
@@ -12,6 +12,7 @@
   val netpair: Proof.context -> Bires.netpair
   val find_rules_netpair: Proof.context -> bool -> thm list -> term -> Bires.netpair -> thm list
   val find_rules: Proof.context -> bool -> thm list -> term -> thm list list
+  val declared_rule: Context.generic -> thm -> bool
   val print_rules: Proof.context -> unit
   val addSWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
   val addWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
@@ -88,6 +89,7 @@
             old_decls netpairs;
       in make_rules decls' netpairs' wrappers end);
 
+
 structure Data = Generic_Data
 (
   type T = rules;
@@ -109,6 +111,10 @@
     in make_rules decls netpairs wrappers end;
 );
 
+fun declared_rule context =
+  let val Rules {decls, ...} =  Data.get context
+  in Bires.has_decls decls end;
+
 fun print_rules ctxt =
   let val Rules {decls, ...} = Data.get (Context.Proof ctxt)
   in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt decls)) end;