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