--- a/src/Pure/Concurrent/future.ML Tue Aug 23 15:48:41 2011 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Aug 23 16:39:21 2011 +0200
@@ -51,7 +51,6 @@
val task_of: 'a future -> task
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
- val get_finished: 'a future -> 'a
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> task list
val cancel: 'a future -> task list
@@ -126,11 +125,6 @@
fun peek x = Single_Assignment.peek (result_of x);
fun is_finished x = is_some (peek x);
-fun get_finished x =
- (case peek x of
- SOME res => Exn.release res
- | NONE => raise Fail "Unfinished future evaluation");
-
(** scheduling **)