diff -r 4d701c0388c3 -r e7e12555e763 NEWS
--- a/NEWS	Mon Sep 06 21:33:19 2010 +0200
+++ b/NEWS	Mon Sep 06 22:08:49 2010 +0200
@@ -232,6 +232,10 @@
 * Configuration option show_question_marks only affects regular pretty
 printing of types and terms, not raw Term.string_of_vname.
 
+* ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare
+INCOMPATIBILITY, superseded by static antiquotations @{thm} and
+@{thms} for most purposes.
+
 * ML structure Unsynchronized never opened, not even in Isar
 interaction mode as before.  Old Unsynchronized.set etc. have been
 discontinued -- use plain := instead.  This should be *rare* anyway,