src/Pure/General/date.scala

     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 Strict
+    {
+      def unapply(s: String): Some[Date] = Some(parse(s))
+    }
   }
 
 
   /* date operations */