author | wenzelm |
Sun, 20 May 2018 15:28:59 +0200 | |
changeset 68230 | 9bee37c2ac2b |
parent 68229 | 18c36ac0acaa |
child 68231 | 0004e7a9fa10 |
--- a/src/Pure/Thy/export_theory.ML Sun May 20 15:24:53 2018 +0200 +++ b/src/Pure/Thy/export_theory.ML Sun May 20 15:28:59 2018 +0200 @@ -20,7 +20,7 @@ if Options.bool (#options context) "export_theory" then f context thy else ())); fun export_body thy name body = - Export.export thy ("theory/" ^ name) [YXML.string_of_body body]; + Export.export thy ("theory/" ^ name) (Buffer.chunks (YXML.buffer_body body Buffer.empty)); (* presentation *)