diff -r 7189368734cd -r be34513a58a1 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sat Jul 05 14:39:24 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sat Jul 05 15:03:26 2025 +0200
@@ -81,13 +81,13 @@
     val th' = Thm.trim_context th;
   in
     make_rules (next - 1) ((w, ((i, b), th')) :: rules)
-      (nth_map i (Bires.insert_tagged_brl ((w, next), (b, th'))) netpairs) wrappers
+      (nth_map i (Bires.insert_tagged_rule ((w, next), (b, th'))) netpairs) wrappers
   end;
 
 fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
   let
     fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
-    fun del b netpair = Bires.delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
+    fun del b netpair = Bires.delete_tagged_rule (b, th) netpair handle Net.DELETE => netpair;
   in
     if not (exists eq_th rules) then rs
     else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
@@ -109,7 +109,7 @@
           k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
       val next = ~ (length rules);
       val netpairs = fold (fn (n, (w, ((i, b), th))) =>
-          nth_map i (Bires.insert_tagged_brl ((w, n), (b, th))))
+          nth_map i (Bires.insert_tagged_rule ((w, n), (b, th))))
         (next upto ~1 ~~ rules) empty_netpairs;
     in make_rules (next - 1) rules netpairs wrappers end;
 );