# HG changeset patch
# User haftmann
# Date 1156345508 -7200
# Node ID f0a5421efb0ba7175d29efeb531c24235efff682
# Parent  8276fd8d19195deb0008bd7be07625fed8dcc4e4
SML/NJ int type fix

diff -r 8276fd8d1919 -r f0a5421efb0b src/HOL/ex/CodeRandom.thy
--- a/src/HOL/ex/CodeRandom.thy	Mon Aug 21 11:02:44 2006 +0200
+++ b/src/HOL/ex/CodeRandom.thy	Wed Aug 23 17:05:08 2006 +0200
@@ -135,19 +135,22 @@
 structure Random : RANDOM =
 struct
 
+open IntInf;
+
 exception RANDOM;
 
-type seed = IntInf.int;
+type seed = int;
 
 local
-  val a = 16807;
-  val m = 2147483647;
+  val a = fromInt 16807;
+    (*greetings to SML/NJ*)
+  val m = (the o fromString) "2147483647";
 in
-  fun next s = IntInf.mod (a * s, m)
+  fun next s = (a * s) mod m;
 end;
 
 local
-  val seed_ref = ref 1;
+  val seed_ref = ref (fromInt 1);
 in
   fun seed () =
     let
@@ -159,7 +162,7 @@
 
 fun value h s =
   if h < 1 then raise RANDOM
-  else (IntInf.mod (s, h - 1), seed ());
+  else (s mod (h - 1), seed ());
 
 end;
 *}