# HG changeset patch
# User wenzelm
# Date 1728997043 -7200
# Node ID 2d73c3287bd3ea27d81d482d40fa3ecb401182ad
# Parent  6b1d5b7ef45e5d2a76fa9edb310dd87c06444c89
backout somewhat pointless 5ea48342e0ae: no need to declare syntax consts for translations (e.g. constraints);

diff -r 6b1d5b7ef45e -r 2d73c3287bd3 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Oct 15 14:55:45 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Oct 15 14:57:23 2024 +0200
@@ -1153,7 +1153,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>
@@ -1214,10 +1214,6 @@
   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
diff -r 6b1d5b7ef45e -r 2d73c3287bd3 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Oct 15 14:55:45 2024 +0200
+++ b/src/Pure/Pure.thy	Tue Oct 15 14:57:23 2024 +0200
@@ -404,7 +404,7 @@
 
 val syntax_consts =
   Parse.and_list1
-    (Scan.optional (Scan.repeat1 Parse.name_position --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) [] --
+    ((Scan.repeat1 Parse.name_position --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) --
       Parse.!!! (Scan.repeat1 Parse.name_position));
 
 val _ =