src/Tools/Metis/PortableIsabelle.sml
changeset 59179 cad8a0012a12
parent 39447 61033a8004e2
child 78650 47d0c333d155
--- a/src/Tools/Metis/PortableIsabelle.sml	Mon Dec 22 18:10:54 2014 +0100
+++ b/src/Tools/Metis/PortableIsabelle.sml	Mon Dec 22 19:47:58 2014 +0100
@@ -12,7 +12,11 @@
 
 fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y)
 
-fun critical e () = NAMED_CRITICAL "metis" e
+local
+  val lock = Mutex.mutex ();
+in
+  fun critical e () = Multithreading.synchronized "metis" lock e
+end;
 
 val randomWord = Random.nextWord
 val randomBool = Random.nextBool