diff -r 2d16c693d536 -r ef876972fdc1 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Wed Aug 10 14:28:55 2011 +0200
+++ b/src/Pure/Concurrent/bash.ML	Wed Aug 10 15:17:24 2011 +0200
@@ -73,7 +73,7 @@
       in () end;
 
     fun cleanup () =
-     (Simple_Thread.interrupt system_thread;
+     (Simple_Thread.interrupt_unsynchronized system_thread;
       try File.rm script_path;
       try File.rm output_path;
       try File.rm pid_path);