src/Pure/Concurrent/future.ML

--- a/src/Pure/Concurrent/future.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/future.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -202,14 +202,14 @@
   let
     val running = Task_Queue.cancel (! queue) group;
     val _ = running |> List.app (fn thread =>
-      if Standard_Thread.is_self thread then ()
-      else Standard_Thread.interrupt_unsynchronized thread);
+      if Isabelle_Thread.is_self thread then ()
+      else Isabelle_Thread.interrupt_unsynchronized thread);
   in running end;
 
 fun cancel_all () = (*requires SYNCHRONIZED*)
   let
     val (groups, threads) = Task_Queue.cancel_all (! queue);
-    val _ = List.app Standard_Thread.interrupt_unsynchronized threads;
+    val _ = List.app Isabelle_Thread.interrupt_unsynchronized threads;
   in groups end;
 
 fun cancel_later group = (*requires SYNCHRONIZED*)
@@ -280,7 +280,7 @@
       Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
     val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
     val worker =
-      Standard_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
+      Isabelle_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
         (fn () => worker_loop name);
   in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
   handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
@@ -383,7 +383,7 @@
   if scheduler_active () then ()
   else
     scheduler :=
-      SOME (Standard_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
+      SOME (Isabelle_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
         scheduler_loop));