--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 23 20:40:20 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 23 21:15:11 2012 +0100
@@ -2351,7 +2351,7 @@
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
-\rail@nont{\isa{name}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
\rail@endbar
\rail@bar
@@ -2408,7 +2408,7 @@
\rail@end
\rail@begin{4}{}
\rail@term{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}}[]
-\rail@nont{\isa{typeconstructor}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@cr{2}
\rail@term{\isa{operations{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@plus
@@ -2420,7 +2420,7 @@
\rail@term{\hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\isa{theoryname}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@endbar
\rail@end
\rail@begin{2}{\isa{modes}}