# HG changeset patch
# User wenzelm
# Date 1267973389 -3600
# Node ID 6cec06ef67a79f86a493966c8176dff787c37446
# Parent  06197484c6ad1975bac1ab4115d8cfa959c0acf4
proper int wrapping for Word32;

diff -r 06197484c6ad -r 6cec06ef67a7 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Sun Mar 07 12:47:02 2010 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML	Sun Mar 07 15:49:49 2010 +0100
@@ -165,6 +165,15 @@
   val fromInt = Word.fromInt o dest_int;
 end;
 
+structure Word32 =
+struct
+  open Word32;
+  val wordSize = mk_int Word32.wordSize;
+  val toInt = mk_int o Word32.toInt;
+  val toIntX = mk_int o Word32.toIntX;
+  val fromInt = Word32.fromInt o dest_int;
+end;
+
 
 (* Real *)