clarified signature (again);

--- a/src/Pure/System/isabelle_system.scala	Mon Apr 12 22:26:30 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Apr 12 22:36:13 2021 +0200
@@ -127,7 +127,7 @@
           if (rc != 0) error(output)
 
           val entries =
-            (for (entry <- Library.split_strings0(File.read(dump)) if entry != "") yield {
+            (for (entry <- space_explode('\u0000', File.read(dump)) if entry != "") yield {
               val i = entry.indexOf('=')
               if (i <= 0) entry -> ""
               else entry.substring(0, i) -> entry.substring(i + 1)

--- 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