# HG changeset patch
# User wenzelm
# Date 1316792106 -7200
# Node ID d5156aa8556d04ab001e3770155ff29bd07a54c5
# Parent  11f622794ad6d8cbe5b6909cf2757b2395d434c9
made SML/NJ happy;

diff -r 11f622794ad6 -r d5156aa8556d 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;