diff -r 8bf765c9c2e5 -r 2c76c66897fc src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Thu Feb 04 21:22:53 2016 +0100
+++ b/src/Pure/GUI/gui_thread.scala	Thu Feb 04 21:28:56 2016 +0100
@@ -49,9 +49,9 @@
 
   /* delayed events */
 
-  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
-    : Standard_Thread.Delay = Standard_Thread.delay_first(delay, cancel) { later { event } }
+  def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
+    Standard_Thread.delay_first(delay) { later { event } }
 
-  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
-    : Standard_Thread.Delay = Standard_Thread.delay_last(delay, cancel) { later { event } }
+  def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
+    Standard_Thread.delay_last(delay) { later { event } }
 }