src/Tools/Metis/metis.ML
changeset 78650 47d0c333d155
parent 74358 6ab3116a251a
--- a/src/Tools/Metis/metis.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Tools/Metis/metis.ML	Wed Sep 06 20:51:28 2023 +0200
@@ -154,7 +154,7 @@
 fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y)
 
 local
-  val lock = Mutex.mutex ();
+  val lock = Thread.Mutex.mutex ();
 in
   fun critical e () = Multithreading.synchronized "metis" lock e
 end;