1.1 --- a/src/Pure/library.ML	Fri Aug 03 20:19:41 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Aug 03 22:33:03 2007 +0200
     1.3 @@ -1030,7 +1030,7 @@
     1.4  val gensym_seed = ref 0;
     1.5  
     1.6  in
     1.7 -  fun gensym pre = pre ^ newid (CRITICAL (fn () => inc gensym_seed));
     1.8 +  fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
     1.9  end;
    1.10  
    1.11  
    1.12 @@ -1041,7 +1041,7 @@
    1.13  
    1.14  type serial = int;
    1.15  local val count = ref 0
    1.16 -in fun serial () = CRITICAL (fn () => inc count) end;
    1.17 +in fun serial () = NAMED_CRITICAL "serial" (fn () => inc count) end;
    1.18  
    1.19  val serial_string = string_of_int o serial;
    1.20