src/Pure/library.ML
changeset 24023 6fd65e2e0dba
parent 23963 c2ee97a963db
child 24049 e4adf8175149
     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