# HG changeset patch
# User wenzelm
# Date 1187436746 -7200
# Node ID 9625e5bfa456bd2a290b9e9944683b98599e6947
# Parent  9aa7b5708eac46d193db6465aa5fd68aa05491a4
NAMED_CRITICAL;

diff -r 9aa7b5708eac -r 9625e5bfa456 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Sat Aug 18 13:32:25 2007 +0200
+++ b/src/Tools/Metis/metis.ML	Sat Aug 18 13:32:26 2007 +0200
@@ -82,7 +82,7 @@
 (* Critical section markup (multiprocessing)                                 *)
 (* ------------------------------------------------------------------------- *)
 
-val CRITICAL = CRITICAL;
+fun CRITICAL e = NAMED_CRITICAL "metis" e;
 
 end
 
diff -r 9aa7b5708eac -r 9625e5bfa456 src/Tools/Metis/src/PortableIsabelle.sml
--- a/src/Tools/Metis/src/PortableIsabelle.sml	Sat Aug 18 13:32:25 2007 +0200
+++ b/src/Tools/Metis/src/PortableIsabelle.sml	Sat Aug 18 13:32:26 2007 +0200
@@ -27,7 +27,7 @@
 (* Critical section markup (multiprocessing)                                 *)
 (* ------------------------------------------------------------------------- *)
 
-val CRITICAL = CRITICAL;
+fun CRITICAL e = NAMED_CRITICAL "metis" e;
 
 end