doc-src/IsarRef/Thy/document/HOL_Specific.tex

 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@endbar
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@end
 \rail@begin{2}{\isa{abstype}}
-\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
+\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}}}}[]
 \rail@endbar
 \rail@end

   \end{matharray}
 
   \begin{railoutput}
 \rail@begin{4}{}
 \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
-\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
+\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
 \rail@cr{2}
 \rail@bar
 \rail@nextbar{3}
 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

   \begin{railoutput}
 \rail@begin{2}{}
 \rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \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.term}{\mbox{\isa{term}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\isa{rule}}[]

 \rail@end
 \rail@begin{3}{}
 \rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \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@bar
 \rail@nextbar{1}
 \rail@plus
 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]