diff -r e61b0b819d28 -r c95edf19133b src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Jan 13 20:25:41 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Mon Jan 14 13:58:12 2019 +0100
@@ -177,7 +177,7 @@
       ());
 
 fun export_information thy name content =
-  (Export.export thy name [content]; Export.information thy "");
+  (Export.export thy name [content]; writeln (Export.message thy ""));
 
 fun export_to_exports thy width (Singleton (extension, p)) =
       export_information thy (generatedN ^ "." ^ extension) (Code_Printer.format [] width p)