clarified modules;

--- a/src/Pure/Isar/context_rules.ML	Wed Jul 09 17:00:03 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Thu Jul 10 12:40:45 2025 +0200
@@ -90,12 +90,8 @@
 );
 
 fun print_rules ctxt =
-  let
-    val Rules {decls, ...} = Data.get (Context.Proof ctxt);
-    fun prt_kind kind =
-      Pretty.big_list (Bires.kind_title kind ^ ":")
-        (Bires.print_decls kind decls |> map (fn (th, _) => Thm.pretty_thm_item ctxt th));
-  in Pretty.writeln (Pretty.chunks (map prt_kind Bires.kind_domain)) end;
+  let val Rules {decls, ...} = Data.get (Context.Proof ctxt)
+  in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt Bires.kind_domain decls)) end;
 
 
 (* access data *)

--- a/src/Pure/bires.ML	Wed Jul 09 17:00:03 2025 +0200
+++ b/src/Pure/bires.ML	Thu Jul 10 12:40:45 2025 +0200
@@ -40,7 +40,7 @@
   type 'a decls
   val has_decls: 'a decls -> thm -> bool
   val list_decls: (thm * 'a decl -> bool) -> 'a decls -> (thm * 'a decl) list
-  val print_decls: kind -> 'a decls -> (thm * 'a decl) list
+  val pretty_decls: Proof.context -> kind list -> 'a decls -> Pretty.T list
   val merge_decls: 'a decls * 'a decls -> (thm * 'a decl) list * 'a decls
   val extend_decls: thm * 'a decl -> 'a decls -> ((thm * 'a decl) * 'a decls) option
   val remove_decls: thm -> 'a decls -> 'a decls option
@@ -178,9 +178,12 @@
 fun list_decls pred =
   dest_decls pred #> sort (rev_order o decl_ord o apply2 #2);
 
-fun print_decls kind =
-  dest_decls (fn (_, {kind = kind', ...}) => kind = kind') #>
-  sort (tag_ord o apply2 (#tag o #2));
+fun pretty_decls ctxt kinds decls =
+  kinds |> map (fn kind =>
+    Pretty.big_list (kind_title kind ^ ":")
+      (dest_decls (fn (_, {kind = kind', ...}) => kind = kind') decls
+        |> sort (tag_ord o apply2 (#tag o #2))
+        |> map (fn (th, _) => Thm.pretty_thm_item ctxt th)));
 
 fun merge_decls (decls1, decls2) =
   decls1 |> fold_map add_decls (list_decls (not o dup_decls decls1) decls2);