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