author | wenzelm |
Wed, 19 Dec 2007 23:49:28 +0100 | |
changeset 25720 | 71e0a5cb2885 |
parent 25719 | a51430528fe0 |
child 25721 | 5ae1dc2bb5ea |
--- a/src/Pure/General/random_word.ML Wed Dec 19 23:42:20 2007 +0100 +++ b/src/Pure/General/random_word.ML Wed Dec 19 23:49:28 2007 +0100 @@ -17,7 +17,7 @@ structure RandomWord: RANDOM_WORD = struct -(*minimal length of unboxed words on all known platforms*) +(*minimum length of unboxed words on all supported ML platforms*) val _ = Word.wordSize >= 30 orelse raise Fail ("Bad platform word size"); val range = 0x40000000;