diff -r 9f30a1238090 -r 0f5fde03e2b5 NEWS
--- a/NEWS	Thu Jun 10 20:12:49 2004 +0200
+++ b/NEWS	Thu Jun 10 20:17:07 2004 +0200
@@ -52,8 +52,7 @@
 * Document preparation: antiquotations now provide the option
   'locale=NAME' to specify an alternative context used for evaluating
   and printing the subsequent argument, as in @{thm [locale=LC]
-  fold_commute}, for example.  Note that a proof context is escaped to
-  the enclosing theory context first.
+  fold_commute}, for example.
 
 * ML: output via the Isabelle channels of writeln/warning/error
   etc. is now passed through Output.output, with a hook for arbitrary