avoid non-portable int constant -- make SML/NJ happy;

--- a/src/Pure/General/socket_io.ML	Wed Oct 16 12:04:38 2013 +0200
+++ b/src/Pure/General/socket_io.ML	Wed Oct 16 12:14:35 2013 +0200
@@ -25,7 +25,7 @@
     val rd =
       BinPrimIO.RD {
         name = name,
-        chunkSize = 4096,
+        chunkSize = io_buffer_size,
         readVec = SOME (fn n => Socket.recvVec (socket, n)),
         readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
         readVecNB = NONE,
@@ -44,7 +44,7 @@
     val wr =
       BinPrimIO.WR {
         name = name,
-        chunkSize = 4096,
+        chunkSize = io_buffer_size,
         writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
         writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
         writeVecNB = NONE,

--- a/src/Pure/ML-Systems/polyml.ML	Wed Oct 16 12:04:38 2013 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Oct 16 12:14:35 2013 +0200
@@ -51,6 +51,8 @@
 val raw_explode = SML90.explode;
 val implode = SML90.implode;
 
+val io_buffer_size = 4096;
+
 fun quit () = exit 0;
 
 

--- a/src/Pure/ML-Systems/smlnj.ML	Wed Oct 16 12:04:38 2013 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Oct 16 12:14:35 2013 +0200
@@ -3,6 +3,7 @@
 Compatibility file for Standard ML of New Jersey.
 *)
 
+val io_buffer_size = 4096;
 use "ML-Systems/proper_int.ML";
 
 exception Interrupt;