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