src/Pure/library.scala

--- a/src/Pure/library.scala	Mon Apr 12 22:26:30 2021 +0200
+++ b/src/Pure/library.scala	Mon Apr 12 22:36:13 2021 +0200
@@ -128,11 +128,6 @@
 
   /* strings */
 
-  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 =
   {
     val s = new StringBuilder