--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sun Oct 18 23:00:32 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sun Oct 18 23:03:43 2015 +0200
@@ -270,7 +270,7 @@
and functor respectively. The source is printed verbatim.
\<^descr> @{text "@{emph s}"} prints document source recursively, with {\LaTeX}
- markup @{verbatim \<open>\emph\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.
+ markup @{verbatim \<open>\emph{\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.
\<^descr> @{text "@{bold s}"} prints document source recursively, with {\LaTeX}
markup @{verbatim \<open>\textbf{\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.