src/Pure/ML-Systems/proper_int.ML

--- a/src/Pure/ML-Systems/proper_int.ML	Fri Sep 23 17:23:54 2011 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML	Fri Sep 23 17:35:06 2011 +0200
@@ -85,6 +85,16 @@
 end;
 
 
+(* Word8VectorSlice *)
+
+structure Word8VectorSlice =
+struct
+  open Word8VectorSlice;
+  val length = mk_int o Word8VectorSlice.length;
+  fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
+end;
+
+
 (* Char *)
 
 structure Char =
@@ -247,6 +257,13 @@
 
 (* Sockets *)
 
+structure Socket =
+struct
+  open Socket;
+  fun recvVec (a, b) = Socket.recvVec (a, dest_int b);
+  fun sendVec a = mk_int (Socket.sendVec a);
+end;
+
 structure INetSock =
 struct
   open INetSock;