src/ZF/QPair.thy

--- a/src/ZF/QPair.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/QPair.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -46,10 +46,10 @@
 
 syntax
   "_QSUM"   :: "[idt, i, i] \<Rightarrow> i"               (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
+syntax_consts
+  "_QSUM" \<rightleftharpoons> QSigma
 translations
   "QSUM x \<in> A. B" => "CONST QSigma(A, \<lambda>x. B)"
-syntax_consts
-  "_QSUM" \<rightleftharpoons> QSigma
 
 abbreviation
   qprod  (infixr \<open><*>\<close> 80) where