diff -r 713424d012fd -r 70076ba563d2 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -40,8 +40,13 @@
 definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
   where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
-syntax "_stuple" :: "[logic, args] \<Rightarrow> logic"  ("(1'(:_,/ _:'))")
-syntax_consts "_stuple" \<rightleftharpoons> spair
+nonterminal stuple_args
+syntax
+  "" :: "logic \<Rightarrow> stuple_args"  ("_")
+  "_stuple_args" :: "logic \<Rightarrow> stuple_args \<Rightarrow> stuple_args"  ("_,/ _")
+  "_stuple" :: "[logic, stuple_args] \<Rightarrow> logic"  ("(1'(:_,/ _:'))")
+syntax_consts
+  "_stuple_args" "_stuple" \<rightleftharpoons> spair
 translations
   "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
   "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"