diff -r 208c99a0092e -r 4d9518c3d031 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Dec 30 21:05:15 2015 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Dec 30 21:10:19 2015 +0100
@@ -101,14 +101,13 @@
   present), including current facts and goals.
 
 
-  All of the diagnostic commands above admit a list of \<open>modes\<close>
-  to be specified, which is appended to the current print mode; see
-  also \secref{sec:print-modes}.  Thus the output behavior may be
-  modified according particular print mode features.  For example,
-  @{command "print_state"}~\<open>(latex xsymbols)\<close> prints the
-  current proof state with mathematical symbols and special characters
-  represented in {\LaTeX} source, according to the Isabelle style
-  @{cite "isabelle-system"}.
+  All of the diagnostic commands above admit a list of \<open>modes\<close> to be
+  specified, which is appended to the current print mode; see also
+  \secref{sec:print-modes}. Thus the output behavior may be modified according
+  particular print mode features. For example, @{command
+  "print_state"}~\<open>(latex)\<close> prints the current proof state with mathematical
+  symbols and special characters represented in {\LaTeX} source, according to
+  the Isabelle style @{cite "isabelle-system"}.
 
   Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
   systematic way to include formal items into the printed text
@@ -278,9 +277,7 @@
   \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active;
   used internally in Isabelle/Pure.
 
-  \<^item> \<^verbatim>\<open>xsymbols\<close>: enable proper mathematical symbols
-  instead of ASCII art.\<^footnote>\<open>This traditional mode name stems from
-  the ``X-Symbol'' package for classic Proof~General with XEmacs.\<close>
+  \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols.
 
   \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX}
   document preparation of Isabelle theory sources; allows to provide