# HG changeset patch
# User wenzelm
# Date 1186173183 -7200
# Node ID 2d4ee876c215d7ee9f482a8064fd349293a1d839
# Parent  edc90be09ac166077f21538528f0009b03ab451a
named some CRITICAL sections;

diff -r edc90be09ac1 -r 2d4ee876c215 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Aug 03 20:19:41 2007 +0200
+++ b/src/Pure/library.ML	Fri Aug 03 22:33:03 2007 +0200
@@ -1030,7 +1030,7 @@
 val gensym_seed = ref 0;
 
 in
-  fun gensym pre = pre ^ newid (CRITICAL (fn () => inc gensym_seed));
+  fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
 end;
 
 
@@ -1041,7 +1041,7 @@
 
 type serial = int;
 local val count = ref 0
-in fun serial () = CRITICAL (fn () => inc count) end;
+in fun serial () = NAMED_CRITICAL "serial" (fn () => inc count) end;
 
 val serial_string = string_of_int o serial;