diff -r 96722b04f2ae -r 8c8399b9ecaa doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Sat Jul 01 19:58:59 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sat Jul 01 19:59:24 2000 +0200
@@ -362,19 +362,23 @@
 
 \medskip
 
-The following options are available to tune the output.
+The following options are available to tune the output.  Note that some of
+these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
 \begin{descr}
-\item[$show_types = bool$ and $show_sorts = bool$] refer to Isabelle's global
-  ML flags of the same names (see also \cite{isabelle-ref}).
+\item[$show_types = bool$ and $show_sorts = bool$] control printing of
+  explicit type and sort constraints
+\item[$long_names = bool$] forces names of types and constants etc.\ to be
+  printed in their fully qualified internal form.
+\item[$eta_contract = bool$] prints terms in $\eta$-contracted form.
 \item[$display = bool$] indicates if the text is to be output as multi-line
   ``display material'', rather than a small piece of text without line breaks
   (which is the default).
 \item[$quotes = bool$] indicates if the output should be enclosed in double
   quotes.
-\item[$mode = name$] adds $name$ to the print mode to be used for
-  presentation.  Note that the standard setup for {\LaTeX} output is already
-  present by default, including the modes ``$latex$'', ``$xsymbols$'',
-  ``$symbols$''.
+\item[$mode = name$] adds $name$ to the print mode to be used for presentation
+  (see also \cite{isabelle-ref}).  Note that the standard setup for {\LaTeX}
+  output is already present by default, including the modes ``$latex$'',
+  ``$xsymbols$'', ``$symbols$''.
 \item[$margin = nat$] changes the margin for pretty printing of display
   material.
 \end{descr}