--- 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;