# HG changeset patch
# User wenzelm
# Date 1290871672 -3600
# Node ID 889b7545a408098b92801065cfe0f8d3af32ef1c
# Parent  f57ca096d8c935a449e06a0c1ffede8a24c52a5e
more proper int wrappers;

diff -r f57ca096d8c9 -r 889b7545a408 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Sat Nov 27 15:58:36 2010 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML	Sat Nov 27 16:27:52 2010 +0100
@@ -165,6 +165,15 @@
   val fromInt = Word.fromInt o dest_int;
 end;
 
+structure Word8 =
+struct
+  open Word8;
+  val wordSize = mk_int Word8.wordSize;
+  val toInt = mk_int o Word8.toInt;
+  val toIntX = mk_int o Word8.toIntX;
+  val fromInt = Word8.fromInt o dest_int;
+end;
+
 structure Word32 =
 struct
   open Word32;
@@ -174,6 +183,15 @@
   val fromInt = Word32.fromInt o dest_int;
 end;
 
+structure LargeWord =
+struct
+  open LargeWord;
+  val wordSize = mk_int LargeWord.wordSize;
+  val toInt = mk_int o LargeWord.toInt;
+  val toIntX = mk_int o LargeWord.toIntX;
+  val fromInt = LargeWord.fromInt o dest_int;
+end;
+
 
 (* Real *)