--- 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);
--- 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;