diff -r be8c0e039a5e -r bc936d3d8b45 src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/UNITY/Union.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -43,12 +43,12 @@
 syntax
   "_JOIN1"  :: "[pttrns, i] \<Rightarrow> i"     (\<open>(3\<Squnion>_./ _)\<close> 10)
   "_JOIN"   :: "[pttrn, i, i] \<Rightarrow> i"   (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)
+syntax_consts
+  "_JOIN1" "_JOIN" == JOIN
 translations
   "\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))"
   "\<Squnion>x y. B"   == "\<Squnion>x. \<Squnion>y. B"
   "\<Squnion>x. B"     == "CONST JOIN(CONST state, (\<lambda>x. B))"
-syntax_consts
-  "_JOIN1" "_JOIN" == JOIN
 
 
 subsection\<open>SKIP\<close>