diff -r f09f377da49d -r 629558a1ecf5 src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Fri Oct 07 21:19:15 2016 +0200
+++ b/src/Pure/General/date.scala	Fri Oct 07 21:46:42 2016 +0200
@@ -59,6 +59,10 @@
     def unapply(str: String): Option[Date] =
       try { Some(parse(str)) }
       catch { case _: DateTimeParseException => None }
+    object Strict
+    {
+      def unapply(s: String): Some[Date] = Some(parse(s))
+    }
   }