1.1 --- a/NEWS	Sat Oct 15 00:09:20 2005 +0200
     1.2 +++ b/NEWS	Sat Oct 15 00:14:30 2005 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 -* Added antiquotations @{ML_type text} and @{ML_struct} which check
     1.8 -the given source text as ML type/structure, printing verbatim.
     1.9 +* Added antiquotations @{ML_type text} and @{ML_struct text} which
    1.10 +check the given source text as ML type/structure, printing verbatim.
    1.11  
    1.12  
    1.13  *** Pure ***