# HG changeset patch
# User blanchet
# Date 1284569557 -7200
# Node ID b42d9885c12962127bb6c45b1d00ee830f443b7e
# Parent  a28be69dcb68743b6f7e0bc6896037fa0bf18877
regenerated "metis.ML"

diff -r a28be69dcb68 -r b42d9885c129 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Wed Sep 15 18:51:48 2010 +0200
+++ b/src/Tools/Metis/metis.ML	Wed Sep 15 18:52:37 2010 +0200
@@ -73,8 +73,7 @@
 
 fun change r f = r := f (!r);
 local val rand = (*Unsynchronized.*)Unsynchronized.ref 0w1
-(* MODIFIED by Jasmin Blanchette *)
-in fun nextWord () = CRITICAL (fn () => ((*Unsynchronized.*)change rand step; ! rand)) end;
+in fun nextWord () = ((*Unsynchronized.*)change rand step; ! rand) end;
 
 (*NB: higher bits are more random than lower ones*)
 fun nextBool () = Word.andb (nextWord (), top_bit) = 0w0;