diff -r c77b9374f45c -r 48baf61cb888 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 20 23:28:35 2010 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 20 23:36:26 2010 +0200
@@ -180,8 +180,8 @@
     val system_thread = Thread.fork (fn () =>
       let
         val status =
-          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" group " ^
-            script_name ^ " " ^ pid_name ^ " " ^ output_name);
+          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
+            " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
         val res =
           (case Posix.Process.fromStatus status of
             Posix.Process.W_EXITED => Result 0