src/Pure/library.ML

--- a/src/Pure/library.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/library.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -996,9 +996,9 @@
   val random_seed = ref 1.0;
 in
 
-fun random () =
-  let val r = rmod (a * !random_seed) m
-  in (random_seed := r; r) end;
+fun random () = CRITICAL (fn () =>
+  let val r = rmod (a * ! random_seed) m
+  in (random_seed := r; r) end);
 
 end;
 
@@ -1062,7 +1062,7 @@
 val gensym_seed = ref 0;
 
 in
-  fun gensym pre = pre ^ newid (inc gensym_seed);
+  fun gensym pre = pre ^ newid (CRITICAL (fn () => inc gensym_seed));
 end;
 
 
@@ -1073,7 +1073,7 @@
 
 type serial = int;
 local val count = ref 0
-in fun serial () = inc count end;
+in fun serial () = CRITICAL (fn () => inc count) end;
 
 val serial_string = string_of_int o serial;