diff -r 91703452523d -r b70d82358c6d src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Mar 01 17:44:44 2021 +0100
+++ b/src/Pure/library.scala	Mon Mar 01 18:11:06 2021 +0100
@@ -126,6 +126,9 @@
 
   /* strings */
 
+  def cat_strings0(strs: TraversableOnce[String]): String = strs.mkString("\u0000")
+  def split_strings0(str: String): List[String] = space_explode('\u0000', str)
+
   def make_string(f: StringBuilder => Unit): String =
   {
     val s = new StringBuilder