src/Pure/library.scala

--- a/src/Pure/library.scala	Thu Mar 04 15:52:08 2021 +0100
+++ b/src/Pure/library.scala	Thu Mar 04 15:59:28 2021 +0100
@@ -96,9 +96,11 @@
 
   /* lines */
 
-  def terminate_lines(lines: IterableOnce[String]): String = lines.mkString("", "\n", "\n")
+  def terminate_lines(lines: IterableOnce[String]): String =
+    lines.iterator.mkString("", "\n", "\n")
 
-  def cat_lines(lines: IterableOnce[String]): String = lines.mkString("\n")
+  def cat_lines(lines: IterableOnce[String]): String =
+    lines.iterator.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
@@ -126,7 +128,9 @@
 
   /* strings */
 
-  def cat_strings0(strs: IterableOnce[String]): String = strs.mkString("\u0000")
+  def cat_strings0(strs: IterableOnce[String]): String =
+    strs.iterator.mkString("\u0000")
+
   def split_strings0(str: String): List[String] = space_explode('\u0000', str)
 
   def make_string(f: StringBuilder => Unit): String =