1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Mar 17 17:58:40 2012 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sat Mar 17 22:46:19 2012 +0100
     1.3 @@ -148,13 +148,13 @@
     1.4    \begin{railoutput}
     1.5  \rail@begin{1}{}
     1.6  \rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
     1.7 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
     1.8 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
     1.9  \rail@term{\isa{\isakeyword{begin}}}[]
    1.10  \rail@end
    1.11  \rail@begin{1}{\indexdef{}{syntax}{target}\hypertarget{syntax.target}{\hyperlink{syntax.target}{\mbox{\isa{target}}}}}
    1.12  \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
    1.13  \rail@term{\isa{\isakeyword{in}}}[]
    1.14 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    1.15 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
    1.16  \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
    1.17  \rail@end
    1.18  \end{railoutput}