src/Pure/General/random_word.ML
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;