setmp: NAMED_CRITICAL;
authorwenzelm
Sat Jul 28 20:40:29 2007 +0200 (2007-07-28)
changeset 240236fd65e2e0dba
parent 24022 ab76c73b3b58
child 24024 c46bd50df3f9
setmp: NAMED_CRITICAL;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sat Jul 28 20:40:27 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Sat Jul 28 20:40:29 2007 +0200
     1.3 @@ -338,7 +338,7 @@
     1.4      val _ = flag := orig_value;
     1.5    in Exn.release result end;
     1.6  
     1.7 -fun setmp flag value f x = CRITICAL (fn () => setmp_noncritical flag value f x);
     1.8 +fun setmp flag value f x = NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
     1.9  
    1.10  
    1.11