src/Pure/Pure.thy

--- a/src/Pure/Pure.thy	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Pure.thy	Fri Apr 25 11:22:25 2025 +0200
@@ -1155,7 +1155,7 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_context\<close>
     "print context of local theory target"
-    (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
+    (Scan.succeed (Toplevel.keep (Pretty.writeln o Pretty.chunks o Toplevel.pretty_context)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_theory\<close>
@@ -1275,7 +1275,7 @@
     "print term bindings of proof context"
     (Scan.succeed
       (Toplevel.keep
-        (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
+        (Pretty.writeln o Pretty.chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_facts\<close> "print facts of proof context"
@@ -1285,7 +1285,8 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_cases\<close> "print cases of proof context"
     (Scan.succeed
-      (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
+      (Toplevel.keep
+        (Pretty.writeln o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_statement\<close>
@@ -1411,7 +1412,7 @@
                 NONE => (Theory.parents_of thy, [thy])
               | SOME (xs, NONE) => (map check xs, [thy])
               | SOME (xs, SOME ys) => (map check xs, map check ys))
-            |> map pretty_thm |> Pretty.writeln_chunks
+            |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
           end)));
 
 in end\<close>