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;