diff -r 099518e8af2c -r 7a273824e206 src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Sat Oct 08 10:59:38 2016 +0200
+++ b/src/Pure/General/date.scala	Sat Oct 08 11:04:47 2016 +0200
@@ -19,29 +19,6 @@
 {
   /* format */
 
-  object Formatter
-  {
-    def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
-
-    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(_))
-      })
-
-    @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
-      last_exn: Option[DateTimeParseException] = None): TemporalAccessor =
-    {
-      fmts match {
-        case Nil =>
-          throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0))
-        case fmt :: rest =>
-          try { ZonedDateTime.from(fmt.parse(str)) }
-          catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) }
-      }
-    }
-  }
-
   object Format
   {
     def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
@@ -76,6 +53,29 @@
     }
   }
 
+  object Formatter
+  {
+    def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
+
+    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(_))
+      })
+
+    @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
+      last_exn: Option[DateTimeParseException] = None): TemporalAccessor =
+    {
+      fmts match {
+        case Nil =>
+          throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0))
+        case fmt :: rest =>
+          try { ZonedDateTime.from(fmt.parse(str)) }
+          catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) }
+      }
+    }
+  }
+
 
   /* date operations */