src/Pure/Thy/export_theory.ML
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 *)