# HG changeset patch
# User wenzelm
# Date 1248689818 -7200
# Node ID 01ff6781dd18d04fa1d929302745fcaca16077a6
# Parent  9a2566d1fdbd88210e1013e864f571ccaaa3acf8
tuned;

diff -r 9a2566d1fdbd -r 01ff6781dd18 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Jul 27 12:11:18 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Jul 27 12:16:58 2009 +0200
@@ -11,7 +11,7 @@
     processes.
 
   * Futures are grouped; failure of one group member causes the whole
-    group to be interrupted eventually.
+    group to be interrupted eventually.  Groups are block-structured.
 
   * Forked futures are evaluated spontaneously by a farm of worker
     threads in the background; join resynchronizes the computation and
@@ -248,9 +248,9 @@
       else
         (case List.partition (Thread.isActive o #1) (! workers) of
           (_, []) => ()
-        | (active, inactive) =>
-            (workers := active; Multithreading.tracing 0 (fn () =>
-              "SCHEDULE: disposed " ^ string_of_int (length inactive) ^ " dead worker threads")));
+        | (alive, dead) =>
+            (workers := alive; Multithreading.tracing 0 (fn () =>
+              "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads")));
     val _ = trace_active ();
 
     val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();