--- 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