# HG changeset patch
# User wenzelm
# Date 1419274078 -3600
# Node ID cad8a0012a126ea895c2d355520e90989fa72331
# Parent  e819a6683f87e9583cf0e2bdd0d136967065d907
more elementary Multithreading.synchronized;

diff -r e819a6683f87 -r cad8a0012a12 src/Tools/Metis/PortableIsabelle.sml
--- 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
diff -r e819a6683f87 -r cad8a0012a12 src/Tools/Metis/metis.ML
--- 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