src/Doc/Isar_Ref/Inner_Syntax.thy

 
     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
     ;
     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
     ;
-    syntaxdeps: (((@{syntax name}+) ('==' | '\<rightleftharpoons>'))?) (@{syntax name}+)
+    syntaxdeps: (@{syntax name}+) ('==' | '\<rightleftharpoons>') (@{syntax name}+)
     ;
     transpat: ('(' @{syntax name} ')')? @{syntax string}
   \<close>
 
   \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without

   wrt.\ formal entities of the logic: multiple names may be given on both
   sides. This tells the inner-syntax engine how to markup concrete syntax, to
   support hyperlinks in the browser or editor. It is essentially an abstract
   specification of the effect of translation rules (see below) or translation
   functions (see \secref{sec:tr-funs}).
-
-  @{command "syntax_types"}~\<open>types\<close> and @{command "syntax_consts"}~\<open>consts\<close>
-  merely declare formal entities to the inner-syntax engine, without any
-  dependencies yet.
 
   \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules
   (i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The
   theory context maintains two independent lists translation rules: parse
   rules (\<^verbatim>\<open>=>\<close> or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>). For convenience, both