# HG changeset patch
# User wenzelm
# Date 1362479821 -3600
# Node ID 45579fbe5a242400fb880ce7da4d0fb21c111f64
# Parent  6bac04a6a197195c3a8c301e808de49a50d55986
removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);

diff -r 6bac04a6a197 -r 45579fbe5a24 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Mar 05 09:47:15 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Mar 05 11:37:01 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;