src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -268,7 +268,7 @@
   /* content */
 
   def maximum(field: String): Double =
-    (0.0 /: content)({ case (m, e) => m max e.get(field) })
+    content.foldLeft(0.0) { case (m, e) => m max e.get(field) }
 
   def average(field: String): Double =
   {