tuned;

--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Feb 04 15:56:49 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Feb 04 16:08:19 2012 +0100
@@ -339,14 +339,15 @@
   annotations.
 
   @{rail "
-    @{syntax_def mixfix}: '(' (
-      @{syntax string} prios? @{syntax nat}? |
-      (@'infix' | @'infixl' | @'infixr') @{syntax string} @{syntax nat} |
-      @'binder' @{syntax string} prios? @{syntax nat} ) ')'
+    @{syntax_def mixfix}: '(' mfix ')'
     ;
-    @{syntax_def struct_mixfix}: @{syntax mixfix} | '(' @'structure' ')'
+    @{syntax_def struct_mixfix}: '(' ( mfix | @'structure' ) ')'
     ;
 
+    mfix: @{syntax string} prios? @{syntax nat}? |
+      (@'infix' | @'infixl' | @'infixr') @{syntax string} @{syntax nat} |
+      @'binder' @{syntax string} prios? @{syntax nat}
+    ;
     prios: '[' (@{syntax nat} + ',') ']'
   "}
 
@@ -496,10 +497,6 @@
   works within an Isar proof body.
 
   \end{description}
-
-  Note that the more primitive commands @{command "syntax"} and
-  @{command "no_syntax"} (\secref{sec:syn-trans}) provide raw access
-  to the syntax tables of a global theory.
 *}
 
 

--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Feb 04 15:56:49 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Feb 04 16:08:19 2012 +0100
@@ -416,9 +416,22 @@
   annotations.
 
   \begin{railoutput}
-\rail@begin{7}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}}
+\rail@begin{1}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}}
+\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@nont{\isa{mfix}}[]
+\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
+\rail@end
+\rail@begin{2}{\indexdef{}{syntax}{struct\_mixfix}\hypertarget{syntax.struct-mixfix}{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@bar
+\rail@nont{\isa{mfix}}[]
+\rail@nextbar{1}
+\rail@term{\isa{\isakeyword{structure}}}[]
+\rail@endbar
+\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
+\rail@end
+\rail@begin{7}{\isa{mfix}}
+\rail@bar
 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -447,16 +460,6 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
 \rail@endbar
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@end
-\rail@begin{2}{\indexdef{}{syntax}{struct\_mixfix}\hypertarget{syntax.struct-mixfix}{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}}
-\rail@bar
-\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@term{\isa{\isakeyword{structure}}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
 \rail@end
 \rail@begin{2}{\isa{prios}}
 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
@@ -666,11 +669,7 @@
   \item \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but
   works within an Isar proof body.
 
-  \end{description}
-
-  Note that the more primitive commands \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and
-  \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}} (\secref{sec:syn-trans}) provide raw access
-  to the syntax tables of a global theory.%
+  \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %