diff -r 719a02488d25 -r 5ea48342e0ae src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Sep 29 21:20:36 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Sep 29 21:40:37 2024 +0200
@@ -1112,7 +1112,7 @@
     ;
     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>
@@ -1173,6 +1173,10 @@
   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