src/Pure/Concurrent/future.ML

--- a/src/Pure/Concurrent/future.ML	Tue Feb 26 12:50:52 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 26 13:05:48 2013 +0100
@@ -154,10 +154,6 @@
 fun broadcast cond = (*requires SYNCHRONIZED*)
   ConditionVar.broadcast cond;
 
-fun broadcast_work () = (*requires SYNCHRONIZED*)
- (ConditionVar.broadcast work_available;
-  ConditionVar.broadcast work_finished);
-
 end;
 
 
@@ -380,7 +376,7 @@
        (Multithreading.tracing 1 (fn () =>
           string_of_int (length (! canceled)) ^ " canceled groups");
         Unsynchronized.change canceled (filter_out (null o cancel_now));
-        broadcast_work ());
+        signal work_available);
 
 
     (* delay loop *)
@@ -400,7 +396,7 @@
     if Exn.is_interrupt exn then
      (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
       List.app cancel_later (cancel_all ());
-      broadcast_work (); true)
+      signal work_available; true)
     else reraise exn;
 
 fun scheduler_loop () =