diff -r c3f68ea97495 -r d9c112c587f9 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Fri Dec 03 16:39:07 2010 +0100
+++ b/src/Pure/Concurrent/bash.ML	Fri Dec 03 17:16:53 2010 +0100
@@ -64,8 +64,7 @@
       in () end;
 
     fun cleanup () =
-     (terminate ();
-      Simple_Thread.interrupt system_thread;
+     (Simple_Thread.interrupt system_thread;
       try File.rm script_path;
       try File.rm output_path;
       try File.rm pid_path);
@@ -79,6 +78,6 @@
       val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
       val _ = cleanup ();
     in (output, rc) end
-    handle exn => (cleanup (); reraise exn)
+    handle exn => (terminate(); cleanup (); reraise exn)
   end);