more elementary Multithreading.synchronized;

--- 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

--- a/src/Tools/Metis/metis.ML	Mon Dec 22 18:10:54 2014 +0100
+++ b/src/Tools/Metis/metis.ML	Mon Dec 22 19:47:58 2014 +0100
@@ -153,7 +153,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 = Metis_Random.nextWord
 val randomBool = Metis_Random.nextBool