src/Pure/Concurrent/future.ML

     | some => (signal work_available; some));
 
 fun worker_loop name =
   (case SYNCHRONIZED name (fn () => worker_next ()) of
     NONE => ()
-  | SOME work => (execute work; worker_loop name));
+  | SOME work => (Exn.capture Multithreading.interrupted (); execute work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
   Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
     Unsynchronized.ref Working));