diff -r 2eeeced17228 -r a25630deacaf doc-src/IsarRef/Thy/Outer_Syntax.thy
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 22:00:39 2008 +0100
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 22:01:30 2008 +0100
@@ -135,31 +135,45 @@
   \end{supertabular}
   \end{center}
 
-  The syntax of @{syntax string} admits any characters, including
+  A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown,
+  which is internally a pair of base name and index (ML type @{ML_type
+  indexname}).  These components are either separated by a dot as in
+  @{text "?x.1"} or @{text "?x7.3"} or run together as in @{text
+  "?x1"}.  The latter form is possible if the base name does not end
+  with digits.  If the index is 0, it may be dropped altogether:
+  @{text "?x"} and @{text "?x0"} and @{text "?x.0"} all refer to the
+  same unknown, with basename @{text "x"} and index 0.
+
+  The syntax of @{syntax_ref string} admits any characters, including
   newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim
   "\\"}'' (backslash) need to be escaped by a backslash; arbitrary
   character codes may be specified as ``@{verbatim "\\"}@{text ddd}'',
   with three decimal digits.  Alternative strings according to
-  @{syntax altstring} are analogous, using single back-quotes instead.
-  The body of @{syntax verbatim} may consist of any text not
+  @{syntax_ref altstring} are analogous, using single back-quotes
+  instead.
+
+  The body of @{syntax_ref verbatim} may consist of any text not
   containing ``@{verbatim "*"}@{verbatim "}"}''; this allows
-  convenient inclusion of quotes without further escapes.  The greek
-  letters do \emph{not} include @{verbatim "\<lambda>"}, which is already used
-  differently in the meta-logic.
+  convenient inclusion of quotes without further escapes.  There is no
+  way to escape ``@{verbatim "*"}@{verbatim "}"}''.  If the quoted
+  text is {\LaTeX} source, one may usually add some blank or comment
+  to avoid the critical character sequence.
+
+  Source comments take the form @{verbatim "(*"}~@{text
+  "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
+  might prevent this.  Note that this form indicates source comments
+  only, which are stripped after lexical analysis of the input.  The
+  Isar syntax also provides proper \emph{document comments} that are
+  considered as part of the text (see \secref{sec:comments}).
 
   Common mathematical symbols such as @{text \<forall>} are represented in
   Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
   symbols like this, although proper presentation is left to front-end
   tools such as {\LaTeX} or Proof~General with the X-Symbol package.
   A list of standard Isabelle symbols that work well with these tools
-  is given in \cite[appendix~A]{isabelle-sys}.
-  
-  Source comments take the form @{verbatim "(*"}~@{text
-  "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
-  might prevent this.  Note that this form indicates source comments
-  only, which are stripped after lexical analysis of the input.  The
-  Isar syntax also provides proper \emph{document comments} that are
-  considered as part of the text (see \secref{sec:comments}).
+  is given in \cite[appendix~A]{isabelle-sys}.  Note that @{verbatim
+  "\<lambda>"} does not belong to the @{text letter} category, since it is
+  already used differently in the Pure term language.
 *}