changeset 70990 | e5e34bd28257 |
parent 70984 | 5e98925f86ed |
child 70991 | f9f7c34b7dd4 |
--- a/src/Pure/Thy/export_theory.ML Sat Nov 02 10:43:11 2019 +0100 +++ b/src/Pure/Thy/export_theory.ML Sat Nov 02 10:56:53 2019 +0100 @@ -129,8 +129,8 @@ if Buffer.is_empty buffer then () else Export.export thy (Path.binding0 (Path.make ["theory", name])) (Buffer.chunks buffer); -fun export_body thy name elems = - export_buffer thy name (YXML.buffer_body elems Buffer.empty); +fun export_body thy name body = + export_buffer thy name (fold YXML.buffer body Buffer.empty); (* presentation *)