1.1 --- a/NEWS	Thu Jun 03 16:39:05 2010 +0200
     1.2 +++ b/NEWS	Thu Jun 03 16:39:50 2010 +0200
     1.3 @@ -140,8 +140,8 @@
     1.4  within a local theory context.  Minor INCOMPATIBILITY.
     1.5  
     1.6  * Proof terms: Type substitutions on proof constants now use canonical
     1.7 -order of type variables. Potential INCOMPATIBILITY for tools working
     1.8 -with proof terms.
     1.9 +order of type variables.  INCOMPATIBILITY for tools working with proof
    1.10 +terms.
    1.11  
    1.12  * New operation Thm.unconstrainT eliminates all sort constraints from
    1.13  a theorem and proof, introducing explicit OFCLASS-premises. On the