diff -r 54085e37ce4d -r 6676bf189852 NEWS
--- a/NEWS	Thu Oct 28 20:32:40 2021 +0200
+++ b/NEWS	Thu Oct 28 20:38:21 2021 +0200
@@ -340,9 +340,6 @@
 adoption; better use TVars.add, TVars.add_tfrees etc. for scalable
 accumulation of items.
 
-* ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
-corresponding ML values, notably as arguments for Thm.instantiate etc.
-
 * ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
 corresponding functions for the object-logic of the ML compilation
 context. This supersedes older mk_Trueprop / dest_Trueprop operations.