diff -r 029400b6c893 -r f99ec71de82d NEWS
--- a/NEWS	Fri Oct 29 11:04:41 2010 +0200
+++ b/NEWS	Fri Oct 29 11:07:21 2010 +0200
@@ -344,6 +344,10 @@
 Fail if the argument is false.  Due to inlining the source position of
 failed assertions is included in the error output.
 
+* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
+text is in practice always evaluated with a stable theory checkpoint.
+Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
+
 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
 meaning.