--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Thu May 05 23:23:02 2011 +0200
@@ -432,7 +432,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@end
-\rail@begin{6}{\indexdef{}{syntax}{typespecsorts}\hypertarget{syntax.typespecsorts}{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}}
+\rail@begin{6}{\indexdef{}{syntax}{typespec\_sorts}\hypertarget{syntax.typespec-sorts}{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}}
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}}[]
@@ -472,7 +472,7 @@
This works both for \hyperlink{syntax.term}{\mbox{\isa{term}}} and \hyperlink{syntax.prop}{\mbox{\isa{prop}}}.
\begin{railoutput}
-\rail@begin{2}{\indexdef{}{syntax}{termpat}\hypertarget{syntax.termpat}{\hyperlink{syntax.termpat}{\mbox{\isa{termpat}}}}}
+\rail@begin{2}{\indexdef{}{syntax}{term\_pat}\hypertarget{syntax.term-pat}{\hyperlink{syntax.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}}}}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
\rail@plus
\rail@term{\isa{\isakeyword{is}}}[]
@@ -481,7 +481,7 @@
\rail@endplus
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@end
-\rail@begin{2}{\indexdef{}{syntax}{proppat}\hypertarget{syntax.proppat}{\hyperlink{syntax.proppat}{\mbox{\isa{proppat}}}}}
+\rail@begin{2}{\indexdef{}{syntax}{prop\_pat}\hypertarget{syntax.prop-pat}{\hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}}}}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
\rail@plus
\rail@term{\isa{\isakeyword{is}}}[]
@@ -522,7 +522,7 @@
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.proppat}{\mbox{\isa{proppat}}}}[]
+\rail@nont{\hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}}}[]
\rail@endbar
\rail@nextplus{2}
\rail@endplus