diff -r 3e099fc47afd -r 9cb1b484fe96 NEWS
--- a/NEWS	Sat Mar 01 14:10:13 2008 +0100
+++ b/NEWS	Sat Mar 01 14:10:14 2008 +0100
@@ -112,6 +112,9 @@
 
 *** ML ***
 
+* ML within Isar: antiquotation @{const name} or @{const
+name(typargs)} produces statically-checked Const term.
+
 * The ``print mode'' is now a thread-local value derived from a global
 template (the former print_mode reference), thus access becomes
 non-critical.  The global print_mode reference is for session