--- 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;
+