src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -54,7 +54,7 @@
     consume: Properties.T => Unit = Console.println
   ): Unit = {
     def progress_stdout(line: String): Unit = {
-      val props = Library.space_explode(',', line).flatMap(Properties.Eq.unapply)
+      val props = space_explode(',', line).flatMap(Properties.Eq.unapply)
       if (props.nonEmpty) consume(props)
     }