
diff -r 3f19e324ff59 -r 528a2ba8fa74 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu May 05 23:23:02 2011 +0200
@@ -358,7 +358,7 @@
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\indexdef{}{syntax}{structmixfix}\hypertarget{syntax.structmixfix}{\hyperlink{syntax.structmixfix}{\mbox{\isa{structmixfix}}}}}
+\rail@begin{2}{\indexdef{}{syntax}{struct\_mixfix}\hypertarget{syntax.struct-mixfix}{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}}
 \rail@bar
 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
 \rail@nextbar{1}
@@ -527,7 +527,7 @@
 \rail@cr{3}
 \rail@plus
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@nont{\hyperlink{syntax.structmixfix}{\mbox{\isa{structmixfix}}}}[]
+\rail@nont{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}[]
 \rail@nextplus{4}
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
@@ -540,7 +540,7 @@
 \rail@endbar
 \rail@plus
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@nont{\hyperlink{syntax.structmixfix}{\mbox{\isa{structmixfix}}}}[]
+\rail@nont{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}[]
 \rail@nextplus{1}
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus




