changeset 56334 | 6b3739fee456 |
parent 56304 | 40274e4f5ebf |
child 56438 | 7f6b2634d853 |
--- a/src/Pure/Thy/thy_output.ML Mon Mar 31 10:28:08 2014 +0200 +++ b/src/Pure/Thy/thy_output.ML Mon Mar 31 12:35:39 2014 +0200 @@ -109,7 +109,7 @@ in [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names), Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)] - |> Pretty.chunks |> Pretty.writeln + |> Pretty.writeln_chunks end; fun antiquotation name scan body =