--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Dec 13 20:29:59 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Dec 13 23:23:51 2011 +0100
@@ -1036,7 +1036,7 @@
\rail@endplus
\rail@end
\rail@begin{2}{\isa{spec}}
-\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
+\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]