diff -r ed24ba6f69aa -r 0991c84e8dcf NEWS
--- a/NEWS	Mon Feb 15 17:17:51 2010 +0100
+++ b/NEWS	Mon Feb 15 18:03:42 2010 +0100
@@ -10,7 +10,9 @@
 the user space functionality any longer.
 
 * Discontinued unnamed infix syntax (legacy feature for many years) --
-need to specify constant name and syntax separately.
+need to specify constant name and syntax separately.  Internal ML
+datatype constructors have been renamed from InfixName to Infix etc.
+Minor INCOMPATIBILITY.
 
 
 *** HOL ***