# HG changeset patch
# User wenzelm
# Date 1618259773 -7200
# Node ID a30a60aef59fd15283ea08cc9049b6deaba66e43
# Parent  6ab97ac63809f8ec5c8dea2f3138e90d9dd092d2
clarified signature (again);

diff -r 6ab97ac63809 -r a30a60aef59f src/Pure/System/isabelle_system.scala
--- 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)
diff -r 6ab97ac63809 -r a30a60aef59f 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