diff -r 8b165615ffe3 -r a4051679a7bf src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Nov 11 20:50:12 2013 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Nov 11 21:04:30 2013 +0100
@@ -105,7 +105,7 @@
 
     val writeln_buffer = Unsynchronized.ref Buffer.empty;
     fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
-    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
+    fun output_writeln () = writeln (trim_line (Buffer.content (! writeln_buffer)));
 
     val warnings = Unsynchronized.ref ([]: string list);
     fun warn msg = Unsynchronized.change warnings (cons msg);