src/Pure/ML/ml_statistics.scala

   }
 
   val empty: ML_Statistics = apply(Nil)
 
   def apply(ml_statistics0: List[Properties.T], heading: String = "",
-    domain: String => Boolean = (key: String) => true): ML_Statistics =
+    domain: String => Boolean = _ => true): ML_Statistics =
   {
     require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
 
     val ml_statistics = ml_statistics0.sortBy(now)
     val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)

 
   /* charts */
 
   def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
   {
-    data.removeAllSeries
+    data.removeAllSeries()
     for (field <- selected_fields) {
       val series = new XYSeries(field)
       content.foreach(entry => series.add(entry.time, entry.get(field)))
       data.addSeries(series)
     }