--- 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;