--- a/NEWS Tue Mar 18 15:29:58 2014 +0100
+++ b/NEWS Tue Mar 18 16:16:28 2014 +0100
@@ -465,10 +465,8 @@
theory merge). Note that the softer Thm.eq_thm_prop is often more
appropriate than Thm.eq_thm.
-* Simplified programming interface to define ML antiquotations (to
-make it more close to the analogous Thy_Output.antiquotation). See
-ML_Context.antiquotation and structure ML_Antiquotation. Minor
-INCOMPATIBILITY.
+* Simplified programming interface to define ML antiquotations, see
+structure ML_Antiquotation. Minor INCOMPATIBILITY.
* ML antiquotation @{here} refers to its source position, which is
occasionally useful for experimentation and diagnostic purposes.