--- 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.