* ML: just one true type int;

--- a/NEWS	Tue Sep 18 18:53:55 2007 +0200
+++ b/NEWS	Wed Sep 19 11:50:07 2007 +0200
@@ -1152,6 +1152,9 @@
 
 *** ML ***
 
+* ML basics: just one true type int, which coincides with IntInf.int
+(even on SML/NJ).
+
 * Generic arithmetic modules: Tools/rat.ML, Tools/float.ML
 
 * Context data interfaces (Theory/Proof/GenericDataFun): removed