diff --git a/src/Pure/General/date.scala b/src/Pure/General/date.scala
--- a/src/Pure/General/date.scala
+++ b/src/Pure/General/date.scala
@@ -1,122 +1,121 @@
 /*  Title:      Pure/General/date.scala
     Author:     Makarius
 
 Date and time, with time zone.
 */
 
 package isabelle
 
 
 import java.util.Locale
-import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime}
+import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId}
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
 import java.time.temporal.TemporalAccessor
 
 import scala.annotation.tailrec
-import scala.math.Ordering
 
 
 object Date
 {
   /* format */
 
   object Format
   {
     def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
     {
       require(fmts.nonEmpty, "no date formats")
 
       new Format {
         def apply(date: Date): String = fmts.head.format(date.rep)
         def parse(str: String): Date =
           new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str))))
       }
     }
 
     def apply(pats: String*): Format =
       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")
     val time: Format = Format("HH:mm:ss")
     val alt_date: Format = Format("uuuuMMdd")
   }
 
   abstract class Format private
   {
     def apply(date: Date): String
     def parse(str: String): Date
 
     def unapply(str: String): Option[Date] =
       try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
   }
 
   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)) }
       }
     }
   }
 
 
   /* ordering */
 
   object Ordering extends scala.math.Ordering[Date]
   {
     def compare(date1: Date, date2: Date): Int =
       date1.instant.compareTo(date2.instant)
   }
 
   object Rev_Ordering extends scala.math.Ordering[Date]
   {
     def compare(date1: Date, date2: Date): Int =
       date2.instant.compareTo(date1.instant)
   }
 
 
   /* date operations */
 
   def timezone_utc: ZoneId = ZoneId.of("UTC")
   def timezone_berlin: ZoneId = ZoneId.of("Europe/Berlin")
 
   def timezone(): ZoneId = ZoneId.systemDefault
 
   def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
 
   def instant(t: Instant, zone: ZoneId = timezone()): Date =
     new Date(ZonedDateTime.ofInstant(t, zone))
 
   def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone)
 }
 
 sealed case class Date(rep: ZonedDateTime)
 {
   def midnight: Date =
     new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
 
   def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
 
   def unix_epoch: Long = rep.toEpochSecond
   def instant: Instant = Instant.from(rep)
   def time: Time = Time.instant(instant)
   def timezone: ZoneId = rep.getZone
 
   def format(fmt: Date.Format = Date.Format.default): String = fmt(this)
   override def toString: String = format()
 }