setmp: NAMED_CRITICAL;
authorwenzelm
Sat, 28 Jul 2007 20:40:29 +0200
changeset 24023 6fd65e2e0dba
parent 24022 ab76c73b3b58
child 24024 c46bd50df3f9
setmp: NAMED_CRITICAL;
src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Jul 28 20:40:27 2007 +0200
+++ b/src/Pure/library.ML	Sat Jul 28 20:40:29 2007 +0200
@@ -338,7 +338,7 @@
     val _ = flag := orig_value;
   in Exn.release result end;
 
-fun setmp flag value f x = CRITICAL (fn () => setmp_noncritical flag value f x);
+fun setmp flag value f x = NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);