src/Pure/Isar/context_rules.ML

--- a/src/Pure/Isar/context_rules.ML	Sat Jul 05 15:03:26 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sat Jul 05 15:53:52 2025 +0200
@@ -77,7 +77,7 @@
 
 fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
   let
-    val w = opt_w |> \<^if_none>\<open>Tactic.subgoals_of_brl (b, th)\<close>;
+    val w = opt_w |> \<^if_none>\<open>Bires.subgoals_of (b, th)\<close>;
     val th' = Thm.trim_context th;
   in
     make_rules (next - 1) ((w, ((i, b), th')) :: rules)