diff -r 63144ea111f7 -r 9cf265a192f6 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Thu Sep 22 20:33:08 2011 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML	Thu Sep 22 21:58:05 2011 +0200
@@ -226,6 +226,16 @@
 end;
 
 
+(* BinIO *)
+
+structure BinIO =
+struct
+  open BinIO;
+  fun inputN (a, b) = BinIO.inputN (a, dest_int b);
+  fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
+end;
+
+
 (* Time *)
 
 structure Time =
@@ -234,3 +244,13 @@
   fun fmt a b = Time.fmt (dest_int a) b;
 end;
 
+
+(* Sockets *)
+
+structure INetSock =
+struct
+  open INetSock;
+  fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
+  fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
+end;
+