diff -r acd3e25975a2 -r 0edc966bee55 src/Pure/Concurrent/event_timer.scala --- a/src/Pure/Concurrent/event_timer.scala Wed Oct 05 14:34:42 2016 +0200 +++ b/src/Pure/Concurrent/event_timer.scala Wed Oct 05 19:45:36 2016 +0200 @@ -11,7 +11,7 @@ package isabelle -import java.util.{Timer, TimerTask, Date} +import java.util.{Timer, TimerTask, Date => JDate} object Event_Timer @@ -26,7 +26,7 @@ def request(time: Time)(event: => Unit): Request = { val task = new TimerTask { def run { event } } - event_timer.schedule(task, new Date(time.ms)) + event_timer.schedule(task, new JDate(time.ms)) new Request(time, task) } }