# HG changeset patch
# User wenzelm
# Date 1357819326 -3600
# Node ID b8ff6d1ee56c037bf817bbb6b6664766109c6f36
# Parent  c0fb2839d1a9b67e1b7b1deb1dcf3cffb56005ab
made SML/NJ happy;

diff -r c0fb2839d1a9 -r b8ff6d1ee56c src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Thu Jan 10 12:41:53 2013 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML	Thu Jan 10 13:02:06 2013 +0100
@@ -257,13 +257,6 @@
 
 (* 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;