--- a/doc-src/Ref/introduction.tex Wed May 03 16:30:39 1995 +0200
+++ b/doc-src/Ref/introduction.tex Wed May 03 16:46:17 1995 +0200
@@ -158,8 +158,8 @@
makes Isabelle show types when printing a term or theorem.
\item[\ttindexbold{show_sorts} := true;]
-makes Isabelle show the sorts of type variables. It has no effect unless
-{\tt show_types} is~{\tt true}.
+makes Isabelle show both types and the sorts of type variables. It does not
+matter whether {\tt show_types} is also~{\tt true}.
\end{ttdescription}