# HG changeset patch
# User blanchet
# Date 1284569481 -7200
# Node ID c551ce5f614a4da3270fb3cf1bab4b31d1973623
# Parent  5d97fd83ab375d7c41b1529278606822c122ae4c
make "Unprotected concurrency introduces some true randomness." be true;
this code is called often and doesn't need to be considered critical. I added CRITICAL by mistake.

diff -r 5d97fd83ab37 -r c551ce5f614a src/Tools/Metis/src/Random.sml
--- a/src/Tools/Metis/src/Random.sml	Wed Sep 15 18:27:29 2010 +0200
+++ b/src/Tools/Metis/src/Random.sml	Wed Sep 15 18:51:21 2010 +0200
@@ -28,8 +28,7 @@
 
 fun change r f = r := f (!r);
 local val rand = (*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;