--- a/src/Doc/System/Sessions.thy Fri Nov 07 16:55:09 2014 +0100
+++ b/src/Doc/System/Sessions.thy Fri Nov 07 17:31:01 2014 +0100
@@ -126,7 +126,7 @@
files that are involved in the processing of this session. This
should cover anything outside the formal content of the theory
sources. In contrast, files that are loaded formally
- within a theory, e.g.\ via @{keyword "ML_file"}, need not be
+ within a theory, e.g.\ via @{command "ML_file"}, need not be
declared again.
\item \isakeyword{document_files}~@{text "("}\isakeyword{in}~@{text