src/Pure/Thy/export_theory.ML
changeset 68230 9bee37c2ac2b
parent 68208 d9f2cf4fc002
child 68231 0004e7a9fa10
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 20 15:24:53 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 20 15:28:59 2018 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4      if Options.bool (#options context) "export_theory" then f context thy else ()));
     1.5  
     1.6  fun export_body thy name body =
     1.7 -  Export.export thy ("theory/" ^ name) [YXML.string_of_body body];
     1.8 +  Export.export thy ("theory/" ^ name) (Buffer.chunks (YXML.buffer_body body Buffer.empty));
     1.9  
    1.10  
    1.11  (* presentation *)