diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -282,7 +282,7 @@
 fun export binding content thy =
   let
     val thy' = thy |> Generated_Files.add_files (binding, content);
-    val _ = Export.export thy' binding [content];
+    val _ = Export.export thy' binding [XML.Text content];
   in thy' end;
 
 local