# HG changeset patch
# User wenzelm
# Date 1312986365 -7200
# Node ID 5d9821493bc16009983ffbe36d3596b8774347c1
# Parent  64634a9ecd466ef9e957123b64efa0ed519eddc2
tuned signature;

diff -r 64634a9ecd46 -r 5d9821493bc1 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Aug 10 16:24:39 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 10 16:26:05 2011 +0200
@@ -39,6 +39,7 @@
   val task_of: 'a future -> Task_Queue.task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
+  val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: Task_Queue.group -> unit
   val cancel: 'a future -> unit
   type fork_params =
@@ -57,7 +58,6 @@
   val promise: unit -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
-  val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val shutdown: unit -> unit
   val status: (unit -> 'a) -> 'a
 end;