--- a/src/Pure/Concurrent/future.ML Tue Mar 05 17:18:02 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Tue Mar 05 17:25:41 2013 +0100
@@ -70,7 +70,6 @@
val value: 'a -> 'a future
val cond_forks: params -> (unit -> 'a) list -> 'a future list
val map: ('a -> 'b) -> 'a future -> 'b future
- val flat: 'a list future list -> 'a list future
val promise_group: group -> (unit -> unit) -> 'a future
val promise: (unit -> unit) -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
@@ -608,20 +607,6 @@
(fn () => f (join x))
end;
-fun flat_future futures =
- (case filter_out is_finished futures of
- [] => value_result (Exn.interruptible_capture (flat o joins) futures)
- | [x] => map_future (fn _ => flat (joins (futures))) x
- | xs =>
- let
- val tasks = map task_of xs;
- val pri = foldl1 Int.min (map Task_Queue.pri_of_task tasks);
- in
- (singleton o cond_forks)
- {name = "flat_future", group = NONE, deps = tasks, pri = pri, interrupts = true}
- (fn () => flat (joins (futures)))
- end);
-
(* promised futures -- fulfilled by external means *)
@@ -705,7 +690,6 @@
(*final declarations of this structure!*)
val map = map_future;
-val flat = flat_future;
end;