diff -r e1b8f2736404 -r 807f6ce0273d NEWS
--- a/NEWS	Fri Jan 22 13:39:00 2010 +0100
+++ b/NEWS	Fri Jan 22 16:56:51 2010 +0100
@@ -12,6 +12,9 @@
 
 *** HOL ***
 
+* HOLogic.strip_psplit: types are returned in syntactic order, similar
+to other strip and tuple operations.  INCOMPATIBILITY.
+
 * Various old-style primrec specifications in the HOL theories have been
 replaced by new-style primrec, especially in theory List.  The corresponding
 constants now have authentic syntax.  INCOMPATIBILITY.