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;