diff -r d682b4000a77 -r f8e52c0152fe src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/GUI/gui_thread.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -58,9 +58,9 @@
 
   /* delayed events */
 
-  def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
-    Standard_Thread.delay_first(delay) { later { event } }
+  def delay_first(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
+    Isabelle_Thread.delay_first(delay) { later { event } }
 
-  def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
-    Standard_Thread.delay_last(delay) { later { event } }
+  def delay_last(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
+    Isabelle_Thread.delay_last(delay) { later { event } }
 }