doc-src/IsarRef/syntax.tex

--- a/doc-src/IsarRef/syntax.tex	Tue Nov 14 09:06:08 2006 +0100
+++ b/doc-src/IsarRef/syntax.tex	Tue Nov 14 15:29:50 2006 +0100
@@ -505,7 +505,7 @@
 \begin{descr}
   
 \item [$\at\{theory~A\}$] prints the name $A$, which is guaranteed to
-  refer to a valid theory in the current session.
+  refer to a valid ancestor theory in the current context.
 
 \item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
   specifications may be included as well (see also \S\ref{sec:syn-att}); the