--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 05 23:23:02 2011 +0200
@@ -283,7 +283,7 @@
 \rail@endbar
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@end