# HG changeset patch
# User wenzelm
# Date 1198104568 -3600
# Node ID 71e0a5cb28855f3997001eb2a1faa9456d1d31d4
# Parent  a51430528fe0e64015ef0a11fffcd2df9ae001a9
tuned comments;

diff -r a51430528fe0 -r 71e0a5cb2885 src/Pure/General/random_word.ML
--- 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;