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;