diff -r 05d2b8b675da -r 57c331dc167d src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Tue Jul 08 12:10:00 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Wed Jul 09 11:09:00 2025 +0200
@@ -40,7 +40,7 @@
 (* context data *)
 
 datatype rules = Rules of
- {decls: Bires.decls,
+ {decls: unit Bires.decls,
   netpairs: Bires.netpair list,
   wrappers:
     ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list *
@@ -52,7 +52,7 @@
 fun add_rule kind opt_weight th (rules as Rules {decls, netpairs, wrappers}) =
   let
     val weight = opt_weight |> \<^if_none>\<open>Bires.subgoals_of (Bires.kind_rule kind th)\<close>;
-    val decl = {kind = kind, tag = Bires.weight_tag weight, implicit = false};
+    val decl = {kind = kind, tag = Bires.weight_tag weight, info = ()};
   in
     (case Bires.extend_decls (Thm.trim_context th, decl) decls of
       NONE => rules