diff -r f718767efd49 -r f8a734dc0fbc doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Jun 22 09:26:18 2005 +0200
@@ -630,8 +630,8 @@
   parsing and type-checking.  Document preparation enables symbolic
   output by default.
 
-  \medskip The next example includes an option to modify Isabelle's
-  \verb,show_types, flag.  The antiquotation
+  \medskip The next example includes an option to show the type of all
+  variables.  The antiquotation
   \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
   output @{term [show_types] "%x y. x"}.  Type inference has figured
   out the most general typings in the present theory context.  Terms