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;