diff -r d8c4a02e992a -r 79ee75dc1e59 NEWS
--- a/NEWS	Sat May 19 11:33:34 2007 +0200
+++ b/NEWS	Sat May 19 11:33:57 2007 +0200
@@ -530,6 +530,10 @@
 
 *** HOL ***
 
+* constant "List.op @" now named "List.append".  Use ML antiquotations
+@{const_name List.append} or @{term " ... @ ... "} to circumvent
+possible incompatibilities when working on ML level.
+
 * Constant renames due to introduction of canonical name prefixing for
   class package: