--- a/src/Doc/Isar_Ref/Document_Preparation.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Jun 22 20:31:49 2018 +0200
@@ -221,8 +221,8 @@
\<^descr> \<open>@{theory_text s}\<close> prints uninterpreted theory source text \<open>s\<close>, i.e.\
outer syntax with command keywords and other tokens.
- \<^descr> \<open>@{theory A}\<close> prints the name \<open>A\<close>, which is guaranteed to refer to a valid
- ancestor theory in the current context.
+ \<^descr> \<open>@{theory A}\<close> prints the session-qualified theory name \<open>A\<close>, which is
+ guaranteed to refer to a valid ancestor theory in the current context.
\<^descr> \<open>@{thm a\<^sub>1 \<dots> a\<^sub>n}\<close> prints theorems \<open>a\<^sub>1 \<dots> a\<^sub>n\<close>. Full fact expressions are
allowed here, including attributes (\secref{sec:syn-att}).