# HG changeset patch
# User wenzelm
# Date 1257685004 -3600
# Node ID b2259183e282cf853b43d63ae32465b30e8ad19b
# Parent  771ec7306438f320fba02f5d716403ae699a99d0
modernized structure Random_Word;

diff -r 771ec7306438 -r b2259183e282 src/Tools/Metis/src/PortableIsabelle.sml
--- a/src/Tools/Metis/src/PortableIsabelle.sml	Sun Nov 08 13:44:16 2009 +0100
+++ b/src/Tools/Metis/src/PortableIsabelle.sml	Sun Nov 08 13:56:44 2009 +0100
@@ -33,10 +33,10 @@
 (* Generating random values.                                                 *)
 (* ------------------------------------------------------------------------- *)
 
-val randomWord = RandomWord.next_word;
-val randomBool = RandomWord.next_bool;
-fun randomInt n = RandomWord.next_int 0 (n - 1);
-val randomReal = RandomWord.next_real;
+val randomWord = Random_Word.next_word;
+val randomBool = Random_Word.next_bool;
+fun randomInt n = Random_Word.next_int 0 (n - 1);
+val randomReal = Random_Word.next_real;
 
 end;
 
diff -r 771ec7306438 -r b2259183e282 src/Tools/random_word.ML
--- a/src/Tools/random_word.ML	Sun Nov 08 13:44:16 2009 +0100
+++ b/src/Tools/random_word.ML	Sun Nov 08 13:56:44 2009 +0100
@@ -18,7 +18,7 @@
   val pick_weighted: (int * 'a) list -> 'a
 end;
 
-structure RandomWord: RANDOM_WORD =
+structure Random_Word: RANDOM_WORD =
 struct
 
 (* random words: 0w0 <= result <= max_word *)