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