# HG changeset patch
# User wenzelm
# Date 1086891427 -7200
# Node ID 0f5fde03e2b5bb336bd4b5d3b294f3547efaa4d4
# Parent  9f30a1238090771c0b89b8789ac328abdbec3871
tuned;

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
diff -r 9f30a1238090 -r 0f5fde03e2b5 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Thu Jun 10 20:12:49 2004 +0200
+++ b/doc-src/IsarRef/syntax.tex	Thu Jun 10 20:17:07 2004 +0200
@@ -532,8 +532,7 @@
 \item[$goals_limit = nat$] determines the maximum number of goals to be
   printed.
 \item[$locale = name$] specifies an alternative context used for evaluating
-  and printing the subsequent argument.  Note that a proof context is escaped
-  to the enclosing theory context first.
+  and printing the subsequent argument.
 \end{descr}
 
 For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''.  All of