diff -r a937889f0086 -r 96e679f042ec src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sat Mar 12 21:23:58 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Sat Mar 12 21:46:31 2016 +0100
@@ -100,14 +100,14 @@
     Bash.process(
       """
         librarypath "$ML_HOME"
-        "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
-        RC="$?"
-
-        [ -e "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
-        rmdir "$ISABELLE_TMP"
-
-        exit "$RC"
-      """, cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect)
+        exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
+      """,
+      cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect,
+      cleanup = () =>
+        {
+          isabelle_process_options.delete
+          Isabelle_System.rm_tree(isabelle_tmp)
+        })
   }