diff -r 46591222e4fc -r 7415414bd9d8 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>\print_context\ "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>\print_theory\ @@ -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>\print_facts\ "print facts of proof context" @@ -1285,7 +1285,8 @@ val _ = Outer_Syntax.command \<^command_keyword>\print_cases\ "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>\print_statement\ @@ -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\