src/Pure/General/date.scala

--- a/src/Pure/General/date.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/date.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -33,7 +33,7 @@
     }
 
     def apply(pats: String*): Format =
-      make(pats.toList.map(Date.Formatter.pattern(_)))
+      make(pats.toList.map(Date.Formatter.pattern))
 
     val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
     val date: Format = Format("dd-MMM-uuuu")
@@ -56,7 +56,7 @@
     def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
       pats.flatMap(pat => {
         val fmt = pattern(pat)
-        if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
+        if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale)
       })
 
     @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,