diff -r 4548b8e1ba12 -r fca432074fb2 NEWS
--- a/NEWS	Wed Nov 09 17:12:26 2011 +0100
+++ b/NEWS	Wed Nov 09 17:57:42 2011 +0100
@@ -16,6 +16,16 @@
 * Redundant attribute 'code_inline' has been discontinued. Use
 'code_unfold' instead. INCOMPATIBILITY.
 
+* Sort constraints are now propagated in simultaneous statements, just
+like type constraints.  INCOMPATIBILITY in rare situations, where
+distinct sorts used to be assigned accidentally.  For example:
+
+  lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"
+
+  lemma "P (x::'a)" and "Q (y::'a::bar)"
+    -- "now uniform 'a::bar instead of default sort for first occurence (!)"
+
+
 
 *** HOL ***