diff -r 3f19e324ff59 -r 528a2ba8fa74 doc-src/IsarRef/Thy/document/Outer_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Thu May 05 23:23:02 2011 +0200
@@ -432,7 +432,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@end
-\rail@begin{6}{\indexdef{}{syntax}{typespecsorts}\hypertarget{syntax.typespecsorts}{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}}
+\rail@begin{6}{\indexdef{}{syntax}{typespec\_sorts}\hypertarget{syntax.typespec-sorts}{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}}
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}}[]
@@ -472,7 +472,7 @@
   This works both for \hyperlink{syntax.term}{\mbox{\isa{term}}} and \hyperlink{syntax.prop}{\mbox{\isa{prop}}}.
 
   \begin{railoutput}
-\rail@begin{2}{\indexdef{}{syntax}{termpat}\hypertarget{syntax.termpat}{\hyperlink{syntax.termpat}{\mbox{\isa{termpat}}}}}
+\rail@begin{2}{\indexdef{}{syntax}{term\_pat}\hypertarget{syntax.term-pat}{\hyperlink{syntax.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}}}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@plus
 \rail@term{\isa{\isakeyword{is}}}[]
@@ -481,7 +481,7 @@
 \rail@endplus
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@end
-\rail@begin{2}{\indexdef{}{syntax}{proppat}\hypertarget{syntax.proppat}{\hyperlink{syntax.proppat}{\mbox{\isa{proppat}}}}}
+\rail@begin{2}{\indexdef{}{syntax}{prop\_pat}\hypertarget{syntax.prop-pat}{\hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}}}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@plus
 \rail@term{\isa{\isakeyword{is}}}[]
@@ -522,7 +522,7 @@
 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.proppat}{\mbox{\isa{proppat}}}}[]
+\rail@nont{\hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}}}[]
 \rail@endbar
 \rail@nextplus{2}
 \rail@endplus