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