changeset 50801 | b8ff6d1ee56c |
parent 45067 | d5156aa8556d |
child 52277 | 2bbeab01c0ea |
--- 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;