# HG changeset patch
# User wenzelm
# Date 1329337763 -3600
# Node ID ea2ae63336f39003b570a129e336dbf601e820ca
# Parent  7e69b9f3149f3943034348a2338985f28c8bb5ba
clarified outer syntax "constdecl", which is only local to some rail diagrams;

diff -r 7e69b9f3149f -r ea2ae63336f3 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy	Wed Feb 15 21:29:23 2012 +0100
@@ -1226,7 +1226,7 @@
   declarations internally.
 
   @{rail "
-    @@{command judgment} @{syntax constdecl}
+    @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?
     ;
     @@{attribute atomize} ('(' 'full' ')')?
     ;
diff -r 7e69b9f3149f -r ea2ae63336f3 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 15 21:29:23 2012 +0100
@@ -864,7 +864,9 @@
 
   @{rail "
     @@{command (HOL) record} @{syntax typespec_sorts} '=' \\
-      (@{syntax type} '+')? (@{syntax constdecl} +)
+      (@{syntax type} '+')? (constdecl +)
+    ;
+    constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
   "}
 
   \begin{description}
diff -r 7e69b9f3149f -r ea2ae63336f3 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Feb 15 21:29:23 2012 +0100
@@ -1038,12 +1038,14 @@
   @{rail "
     @@{command nonterminal} (@{syntax name} + @'and')
     ;
-    (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (@{syntax constdecl} +)
+    (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +)
     ;
     (@@{command translations} | @@{command no_translations})
       (transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +)
     ;
 
+    constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
+    ;
     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
     ;
     transpat: ('(' @{syntax nameref} ')')? @{syntax string}
diff -r 7e69b9f3149f -r ea2ae63336f3 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Wed Feb 15 21:29:23 2012 +0100
@@ -1838,9 +1838,15 @@
   declarations internally.
 
   \begin{railoutput}
-\rail@begin{1}{}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}}[]
-\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
+\rail@endbar
 \rail@end
 \rail@begin{2}{}
 \rail@term{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}}[]
diff -r 7e69b9f3149f -r ea2ae63336f3 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 15 21:29:23 2012 +0100
@@ -1288,10 +1288,19 @@
 \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
 \rail@endbar
 \rail@plus
-\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
+\rail@nont{\isa{constdecl}}[]
 \rail@nextplus{3}
 \rail@endplus
 \rail@end
+\rail@begin{2}{\isa{constdecl}}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
+\rail@endbar
+\rail@end
 \end{railoutput}
 
 
diff -r 7e69b9f3149f -r ea2ae63336f3 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 15 21:29:23 2012 +0100
@@ -1231,7 +1231,7 @@
 \rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]
 \rail@endbar
 \rail@plus
-\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
+\rail@nont{\isa{constdecl}}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
@@ -1260,6 +1260,15 @@
 \rail@nextplus{6}
 \rail@endplus
 \rail@end
+\rail@begin{2}{\isa{constdecl}}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
+\rail@endbar
+\rail@end
 \rail@begin{3}{\isa{mode}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@bar