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