
diff -r ce067c13d8e5 -r f4811f3628dc src/Doc/IsarRef/Outer_Syntax.thy
--- a/src/Doc/IsarRef/Outer_Syntax.thy	Sat Aug 17 22:58:48 2013 +0200
+++ b/src/Doc/IsarRef/Outer_Syntax.thy	Sun Aug 18 13:25:31 2013 +0200
@@ -137,7 +137,7 @@
 
   \begin{center}
   \begin{supertabular}{rcl}
-    @{syntax_def ident} & = & @{text "letter quasiletter\<^sup>*"} \\
+    @{syntax_def ident} & = & @{text "letter (subscript\<^sup>? quasiletter)\<^sup>*"} \\
     @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
     @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
     @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
@@ -150,7 +150,7 @@
     @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*"}@{verbatim "}"} \\[1ex]
 
     @{text letter} & = & @{text "latin  |  "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
-          &   & @{verbatim "\<^sub>"}@{text "  |  "}@{verbatim "\<^sup>"} \\
+    @{text subscript} & = & @{verbatim "\<^sub>"} \\
     @{text quasiletter} & = & @{text "letter  |  digit  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "'"} \\
     @{text latin} & = & @{verbatim a}@{text "  | \<dots> |  "}@{verbatim z}@{text "  |  "}@{verbatim A}@{text "  |  \<dots> |  "}@{verbatim Z} \\
     @{text digit} & = & @{verbatim "0"}@{text "  |  \<dots> |  "}@{verbatim "9"} \\




