src/Pure/library.scala

--- a/src/Pure/library.scala	Mon Oct 03 10:49:27 2016 +0200
+++ b/src/Pure/library.scala	Mon Oct 03 10:51:51 2016 +0200
@@ -99,11 +99,7 @@
 
   /* lines */
 
-  def terminate_lines(lines: Iterable[CharSequence]): Iterable[CharSequence] =
-    new Iterable[CharSequence] {
-      def iterator: Iterator[CharSequence] =
-        lines.iterator.map(line => new Line_Termination(line))
-    }
+  def terminate_lines(lines: TraversableOnce[String]): String = lines.mkString("", "\n", "\n")
 
   def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")