# HG changeset patch
# User wenzelm
# Date 1365508528 -7200
# Node ID 3db1bbc82d8da0685e28784b4b81fb7fce2472cb
# Parent  4ce2f7607d3dcecee0328a07a6ba8f5ca2bbb698
more accurate documentation of "(structure)" mixfix;

diff -r 4ce2f7607d3d -r 3db1bbc82d8d src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Tue Apr 09 13:24:00 2013 +0200
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Tue Apr 09 13:55:28 2013 +0200
@@ -377,13 +377,14 @@
   The string given as @{text template} may include literal text,
   spacing, blocks, and arguments (denoted by ``@{text _}''); the
   special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
-  represents an index argument that specifies an implicit
-  @{text "\<STRUCTURE>"} reference (see also \secref{sec:locale}).  Infix and
-  binder declarations provide common abbreviations for particular mixfix
-  declarations.  So in practice, mixfix templates mostly degenerate to
-  literal text for concrete syntax, such as ``@{verbatim "++"}'' for
-  an infix symbol.
-*}
+  represents an index argument that specifies an implicit @{keyword
+  "structure"} reference (see also \secref{sec:locale}).  Only locally
+  fixed variables may be declared as @{keyword "structure"}.
+
+  Infix and binder declarations provide common abbreviations for
+  particular mixfix declarations.  So in practice, mixfix templates
+  mostly degenerate to literal text for concrete syntax, such as
+  ``@{verbatim "++"}'' for an infix symbol.  *}
 
 
 subsection {* The general mixfix form *}
@@ -836,7 +837,7 @@
   of @{syntax (inner) logic}.
 
   \item @{syntax_ref (inner) index} denotes an optional index term for
-  indexed syntax.  If omitted, it refers to the first @{keyword
+  indexed syntax.  If omitted, it refers to the first @{keyword_ref
   "structure"} variable in the context.  The special dummy ``@{text
   "\<index>"}'' serves as pattern variable in mixfix annotations that
   introduce indexed notation.
diff -r 4ce2f7607d3d -r 3db1bbc82d8d src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Tue Apr 09 13:24:00 2013 +0200
+++ b/src/Doc/IsarRef/Spec.thy	Tue Apr 09 13:55:28 2013 +0200
@@ -514,8 +514,8 @@
   \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
   parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
   are optional).  The special syntax declaration ``@{text
-  "(\<STRUCTURE>)"}'' means that @{text x} may be referenced
-  implicitly in this context.
+  "("}@{keyword_ref "structure"}@{text ")"}'' means that @{text x} may
+  be referenced implicitly in this context.
 
   \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
   constraint @{text \<tau>} on the local parameter @{text x}.  This
diff -r 4ce2f7607d3d -r 3db1bbc82d8d src/Doc/isar.sty
--- a/src/Doc/isar.sty	Tue Apr 09 13:24:00 2013 +0200
+++ b/src/Doc/isar.sty	Tue Apr 09 13:55:28 2013 +0200
@@ -17,7 +17,6 @@
 \newcommand{\isasymBEGIN}{\isakeyword{begin}}
 \newcommand{\isasymIMPORTS}{\isakeyword{imports}}
 \newcommand{\isasymIN}{\isakeyword{in}}
-\newcommand{\isasymSTRUCTURE}{\isakeyword{structure}}
 \newcommand{\isasymFIXES}{\isakeyword{fixes}}
 \newcommand{\isasymASSUMES}{\isakeyword{assumes}}
 \newcommand{\isasymSHOWS}{\isakeyword{shows}}