src/Pure/GUI/gui_thread.scala

--- a/src/Pure/GUI/gui_thread.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/GUI/gui_thread.scala	Tue Nov 03 13:54:34 2015 +0100
@@ -50,8 +50,8 @@
   /* delayed events */
 
   def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
-    : Simple_Thread.Delay = Simple_Thread.delay_first(delay, cancel) { later { event } }
+    : Standard_Thread.Delay = Standard_Thread.delay_first(delay, cancel) { later { event } }
 
   def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
-    : Simple_Thread.Delay = Simple_Thread.delay_last(delay, cancel) { later { event } }
+    : Standard_Thread.Delay = Standard_Thread.delay_last(delay, cancel) { later { event } }
 }