# HG changeset patch
# User wenzelm
# Date 1185648029 -7200
# Node ID 6fd65e2e0dbad6e7e230ce0cf7d6a22ca8676fd3
# Parent  ab76c73b3b5845eedd953811b8c8006ac18c28f2
setmp: NAMED_CRITICAL;

diff -r ab76c73b3b58 -r 6fd65e2e0dba 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);