diff -r 5a12b1b5990f -r 585c1f08499e NEWS
--- a/NEWS	Sat Oct 15 00:09:20 2005 +0200
+++ b/NEWS	Sat Oct 15 00:14:30 2005 +0200
@@ -11,8 +11,8 @@
 
 *** Document preparation ***
 
-* Added antiquotations @{ML_type text} and @{ML_struct} which check
-the given source text as ML type/structure, printing verbatim.
+* Added antiquotations @{ML_type text} and @{ML_struct text} which
+check the given source text as ML type/structure, printing verbatim.
 
 
 *** Pure ***