--- a/NEWS Tue Dec 12 18:53:40 2017 +0100
+++ b/NEWS Wed Dec 13 16:18:40 2017 +0100
@@ -87,12 +87,8 @@
more accurately: only terminal proof steps ('by' etc.) are skipped.
* Command-line tool "isabelle document" has been re-implemented in
-Isabelle/Scala, with simplified arguments. Minor INCOMPATIBILITY.
-
-* Original source positions are inlined into generated tex files: this
-improves error messages by "isabelle document", but may sometimes
-confuse LaTeX. Rare INCOMPATIBILITY, set option
-"document_positions=false" to avoid this.
+Isabelle/Scala, with simplified arguments and explicit errors from the
+latex process. Minor INCOMPATIBILITY.
*** HOL ***