1.1 --- a/src/Pure/Concurrent/future.ML	Tue Mar 05 09:47:15 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Mar 05 11:37:01 2013 +0100
     1.3 @@ -70,7 +70,6 @@
     1.4    val value: 'a -> 'a future
     1.5    val cond_forks: params -> (unit -> 'a) list -> 'a future list
     1.6    val map: ('a -> 'b) -> 'a future -> 'b future
     1.7 -  val flat: 'a list future list -> 'a list future
     1.8    val promise_group: group -> (unit -> unit) -> 'a future
     1.9    val promise: (unit -> unit) -> 'a future
    1.10    val fulfill_result: 'a future -> 'a Exn.result -> unit
    1.11 @@ -608,20 +607,6 @@
    1.12            (fn () => f (join x))
    1.13      end;
    1.14  
    1.15 -fun flat_future futures =
    1.16 -  (case filter_out is_finished futures of
    1.17 -    [] => value_result (Exn.interruptible_capture (flat o joins) futures)
    1.18 -  | [x] => map_future (fn _ => flat (joins (futures))) x
    1.19 -  | xs =>
    1.20 -      let
    1.21 -        val tasks = map task_of xs;
    1.22 -        val pri = foldl1 Int.min (map Task_Queue.pri_of_task tasks);
    1.23 -      in
    1.24 -        (singleton o cond_forks)
    1.25 -          {name = "flat_future", group = NONE, deps = tasks, pri = pri, interrupts = true}
    1.26 -          (fn () => flat (joins (futures)))
    1.27 -      end);
    1.28 -
    1.29  
    1.30  (* promised futures -- fulfilled by external means *)
    1.31  
    1.32 @@ -705,7 +690,6 @@
    1.33  
    1.34  (*final declarations of this structure!*)
    1.35  val map = map_future;
    1.36 -val flat = flat_future;
    1.37  
    1.38  end;
    1.39