--- 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