1.1 --- a/NEWS	Tue Mar 22 17:51:15 2011 +0100
     1.2 +++ b/NEWS	Tue Mar 22 18:03:28 2011 +0100
     1.3 @@ -71,6 +71,14 @@
     1.4  * Path.print is the official way to show file-system paths to users
     1.5  (including quotes etc.).
     1.6  
     1.7 +* Inner syntax: identifiers in parse trees of generic categories
     1.8 +"logic", "aprop", "idt" etc. carry position information (disguised as
     1.9 +type constraints).  Occasional INCOMPATIBILITY with non-compliant
    1.10 +translations that choke on unexpected type constraints: use
    1.11 +Syntax.strip_positions or Syntax.strip_positions_ast.  As last resort,
    1.12 +reset the configuration option Syntax.positions, which is called
    1.13 +"syntax_positions" in Isar attribute source.
    1.14 +
    1.15  
    1.16  
    1.17  New in Isabelle2011 (January 2011)