src/Pure/Concurrent/task_queue.ML

--- a/src/Pure/Concurrent/task_queue.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Sep 06 20:51:28 2023 +0200
@@ -88,7 +88,7 @@
   the_list (! status) @
     (case parent of NONE => [] | SOME group => group_status_unsynchronized group);
 
-val lock = Mutex.mutex ();
+val lock = Thread.Mutex.mutex ();
 fun SYNCHRONIZED e = Multithreading.synchronized "group_status" lock e;
 
 in