1.1 --- a/src/Pure/Concurrent/future.ML	Wed Aug 10 16:24:39 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Aug 10 16:26:05 2011 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    val task_of: 'a future -> Task_Queue.task
     1.5    val peek: 'a future -> 'a Exn.result option
     1.6    val is_finished: 'a future -> bool
     1.7 +  val interruptible_task: ('a -> 'b) -> 'a -> 'b
     1.8    val cancel_group: Task_Queue.group -> unit
     1.9    val cancel: 'a future -> unit
    1.10    type fork_params =
    1.11 @@ -57,7 +58,6 @@
    1.12    val promise: unit -> 'a future
    1.13    val fulfill_result: 'a future -> 'a Exn.result -> unit
    1.14    val fulfill: 'a future -> 'a -> unit
    1.15 -  val interruptible_task: ('a -> 'b) -> 'a -> 'b
    1.16    val shutdown: unit -> unit
    1.17    val status: (unit -> 'a) -> 'a
    1.18  end;