diff -r 9b311dbd0f55 -r 06388a5cfb7c src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Mon Apr 28 00:54:31 2014 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Mon Apr 28 12:56:54 2014 +0200
@@ -9,9 +9,8 @@
 
 signature EVENT_TIMER =
 sig
-  type event = unit -> unit
   eqtype request
-  val request: Time.time -> event -> request
+  val request: Time.time -> (unit -> unit) -> request
   val cancel: request -> bool
   val shutdown: unit -> unit
   val future: Time.time -> unit future
@@ -20,11 +19,6 @@
 structure Event_Timer: EVENT_TIMER =
 struct
 
-(* type event *)
-
-type event = unit -> unit;
-
-
 (* type request *)
 
 val request_counter = Counter.make ();
@@ -35,7 +29,7 @@
 (* type requests *)
 
 structure Requests = Table(type key = Time.time val ord = Time.compare);
-type requests = (request * event) list Requests.table;
+type requests = (request * (unit -> unit)) list Requests.table;
 
 fun add_request time entry (requests: requests) =
   Requests.cons_list (time, entry) requests;