changeset 82587 | 7415414bd9d8 |
parent 81843 | 4329a8fecbe1 |
--- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Apr 25 09:46:21 2025 +0200 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Apr 25 11:22:25 2025 +0200 @@ -88,7 +88,7 @@ Pretty.big_list (name ^ " " ^ f status) (Element.pretty_ctxt ctxt context' @ Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |> - Pretty.writeln_chunks2 + Pretty.chunks2 |> Pretty.writeln end; val _ =