NEWS

--- a/NEWS	Tue Mar 30 15:25:35 2010 +0200
+++ b/NEWS	Tue Mar 30 23:12:55 2010 +0200
@@ -96,6 +96,10 @@
 without introducing dependencies on parameters or assumptions, which
 is not possible in Isabelle/Pure.
 
+* Proof terms: Type substitutions on proof constants now use canonical
+order of type variables. INCOMPATIBILITY: Tools working with proof
+terms may need to be adapted.
+
 
 *** HOL ***