diff -r e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/bash.ML	Tue Nov 03 13:54:34 2015 +0100
@@ -31,7 +31,7 @@
     val _ = cleanup_files ();
 
     val system_thread =
-      Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
         Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
@@ -83,7 +83,7 @@
           in () end;
 
     fun cleanup () =
-     (Simple_Thread.interrupt_unsynchronized system_thread;
+     (Standard_Thread.interrupt_unsynchronized system_thread;
       cleanup_files ());
   in
     let