# HG changeset patch
# User wenzelm
# Date 1724445918 -7200
# Node ID 2c9b5288eb84122c4a029ea8980512a6a713d29a
# Parent  c7f7e58509af9f616dccfe1fb10b1a98afae7644
clarified concrete syntax;

diff -r c7f7e58509af -r 2c9b5288eb84 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 21:32:09 2024 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 22:45:18 2024 +0200
@@ -15,8 +15,10 @@
   val print_ast_translation: Input.source -> theory -> theory
   val translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
-  val syntax_consts: ((string * Position.T) * (xstring * Position.T) list) list -> theory -> theory
-  val syntax_types: ((string * Position.T) * (xstring * Position.T) list) list -> theory -> theory
+  val syntax_consts: ((string * Position.T) list * (xstring * Position.T) list) list ->
+    theory -> theory
+  val syntax_types: ((string * Position.T) list * (xstring * Position.T) list) list ->
+    theory -> theory
   val oracle: bstring * Position.range -> Input.source -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
   val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
@@ -117,13 +119,20 @@
 fun syntax_deps_cmd f args thy =
   let
     val ctxt = Proof_Context.init_global thy;
+
+    val check_lhs = Proof_Context.check_syntax_const ctxt;
     fun check_rhs (b: xstring, pos: Position.T) =
       let
-        val (c, reports) = f ctxt (b, pos);
+        val (c: string, reports) = f ctxt (b, pos);
         val _ = Context_Position.reports ctxt reports;
       in c end;
-    fun check_arg (a, bs) = (Proof_Context.check_syntax_const ctxt a, map check_rhs bs);
-  in Sign.syntax_deps (map check_arg args) thy end;
+
+    fun check (raw_lhs, raw_rhs) =
+      let
+        val lhs = map check_lhs raw_lhs;
+        val rhs = map check_rhs raw_rhs;
+      in map (fn l => (l, rhs)) lhs end;
+  in Sign.syntax_deps (maps check args) thy end;
 
 fun check_const ctxt (s, pos) =
   Proof_Context.check_const {proper = false, strict = true} ctxt (s, [pos])
diff -r c7f7e58509af -r 2c9b5288eb84 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Aug 23 21:32:09 2024 +0200
+++ b/src/Pure/Pure.thy	Fri Aug 23 22:45:18 2024 +0200
@@ -404,7 +404,7 @@
 
 val syntax_consts =
   Parse.and_list1
-    ((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 _ =