src/Tools/WWW_Find/socket_util.ML
changeset 41491 a2ad5b824051
parent 33823 24090eae50b6
child 43703 c37a1f29bbc0
--- a/src/Tools/WWW_Find/socket_util.ML	Mon Jan 10 15:30:17 2011 +0100
+++ b/src/Tools/WWW_Find/socket_util.ML	Mon Jan 10 15:45:46 2011 +0100
@@ -41,7 +41,7 @@
     val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
 
     val sock_name =
-      String.concat [ NetHostDB.toString haddr, ":", Int.toString port ];
+      String.concat [ NetHostDB.toString haddr, ":", string_of_int port ];
 
     val rd =
       BinPrimIO.RD {