diff -r c85e018be3a3 -r e670969f34df NEWS
--- a/NEWS	Mon Dec 08 16:04:50 2014 +0100
+++ b/NEWS	Mon Dec 08 22:42:12 2014 +0100
@@ -218,6 +218,9 @@
 
 *** ML ***
 
+* Cartouches within ML sources are turned into values of type
+Input.source (with formal position information).
+
 * Proper context for various elementary tactics: assume_tac,
 match_tac, compose_tac, Splitter.split_tac etc.  Minor
 INCOMPATIBILITY.