# HG changeset patch
# User wenzelm
# Date 1724591242 -7200
# Node ID bc936d3d8b451ead91ccaf08bfa9c846cdc1e907
# Parent  be8c0e039a5ed82d88998bb2d77ae3d78ce99582
tuned, following be8c0e039a5e;

diff -r be8c0e039a5e -r bc936d3d8b45 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/CCL/Set.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -19,10 +19,10 @@
 
 syntax
   "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  ("(1{_./ _})")
+syntax_consts
+  "_Coll" == Collect
 translations
   "{x. P}" == "CONST Collect(\<lambda>x. P)"
-syntax_consts
-  "_Coll" == Collect
 
 lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}"
   apply (rule mem_Collect_iff [THEN iffD2])
@@ -52,12 +52,12 @@
 syntax
   "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o"  ("(ALL _:_./ _)" [0, 0, 0] 10)
   "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o"  ("(EX _:_./ _)" [0, 0, 0] 10)
+syntax_consts
+  "_Ball" == Ball and
+  "_Bex" == Bex
 translations
   "ALL x:A. P"  == "CONST Ball(A, \<lambda>x. P)"
   "EX x:A. P"   == "CONST Bex(A, \<lambda>x. P)"
-syntax_consts
-  "_Ball" == Ball and
-  "_Bex" == Bex
 
 lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)"
   by (simp add: Ball_def)
@@ -129,12 +129,12 @@
 syntax
   "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  ("(INT _:_./ _)" [0, 0, 0] 10)
   "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  ("(UN _:_./ _)" [0, 0, 0] 10)
+syntax_consts
+  "_INTER" == INTER and
+  "_UNION" == UNION
 translations
   "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)"
   "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)"
-syntax_consts
-  "_INTER" == INTER and
-  "_UNION" == UNION
 
 definition Inter :: "(('a set)set) \<Rightarrow> 'a set"
   where "Inter(S) == (INT x:S. x)"
diff -r be8c0e039a5e -r bc936d3d8b45 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/CCL/Term.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -49,8 +49,8 @@
   where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
 syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
+syntax_consts "_let1" == let1
 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
-syntax_consts "_let1" == let1
 
 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
@@ -68,6 +68,10 @@
   "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
   "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
   "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
+syntax_consts
+  "_letrec" == letrec and
+  "_letrec2" == letrec2 and
+  "_letrec3" == letrec3
 parse_translation \<open>
   let
     fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
@@ -123,10 +127,6 @@
      (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
   end
 \<close>
-syntax_consts
-  "_letrec" == letrec and
-  "_letrec2" == letrec2 and
-  "_letrec3" == letrec3
 
 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
diff -r be8c0e039a5e -r bc936d3d8b45 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/CCL/Type.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -14,10 +14,10 @@
 
 syntax
   "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  ("(1{_: _ ./ _})")
+syntax_consts
+  "_Subtype" == Subtype
 translations
   "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
-syntax_consts
-  "_Subtype" == Subtype
 
 definition Unit :: "i set"
   where "Unit == {x. x=one}"
@@ -39,6 +39,9 @@
   "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set"  ("(3SUM _:_./ _)" [0,0,60] 60)
   "_arrow" :: "[i set, i set] \<Rightarrow> i set"  ("(_ ->/ _)"  [54, 53] 53)
   "_star"  :: "[i set, i set] \<Rightarrow> i set"  ("(_ */ _)" [56, 55] 55)
+syntax_consts
+  "_Pi" "_arrow" \<rightleftharpoons> Pi and
+  "_Sigma" "_star" \<rightleftharpoons> Sigma
 translations
   "PROD x:A. B" \<rightharpoonup> "CONST Pi(A, \<lambda>x. B)"
   "A -> B" \<rightharpoonup> "CONST Pi(A, \<lambda>_. B)"
@@ -50,9 +53,6 @@
   (\<^const_syntax>\<open>Sigma\<close>,
     fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\<open>_Sigma\<close>, \<^syntax_const>\<open>_star\<close>))]
 \<close>
-syntax_consts
-  "_Pi" "_arrow" \<rightleftharpoons> Pi and
-  "_Sigma" "_star" \<rightleftharpoons> Sigma
 
 definition Nat :: "i set"
   where "Nat == lfp(\<lambda>X. Unit + X)"
diff -r be8c0e039a5e -r bc936d3d8b45 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/CTT/CTT.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -58,12 +58,12 @@
 syntax
   "_PROD"   :: "[idt,t,t]\<Rightarrow>t"       ("(3\<Prod>_:_./ _)" 10)
   "_SUM"    :: "[idt,t,t]\<Rightarrow>t"       ("(3\<Sum>_:_./ _)" 10)
+syntax_consts
+  "_PROD" \<rightleftharpoons> Prod and
+  "_SUM" \<rightleftharpoons> Sum
 translations
   "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)"
   "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum(A, \<lambda>x. B)"
-syntax_consts
-  "_PROD" \<rightleftharpoons> Prod and
-  "_SUM" \<rightleftharpoons> Sum
 
 abbreviation Arrow :: "[t,t]\<Rightarrow>t"  (infixr "\<longrightarrow>" 30)
   where "A \<longrightarrow> B \<equiv> \<Prod>_:A. B"
diff -r be8c0e039a5e -r bc936d3d8b45 src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/Cube/Cube.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -39,6 +39,13 @@
   "_Lam" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<^bold>\<lambda>_:_./ _)" [0, 0, 0] 10)
   "_Pi" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<Prod>_:_./ _)" [0, 0] 10)
   "_arrow" :: "[term, term] \<Rightarrow> term"  (infixr "\<rightarrow>" 10)
+syntax_consts
+  "_Trueprop" \<rightleftharpoons> Trueprop and
+  "_MT_context" \<rightleftharpoons> MT_context and
+  "_Context" \<rightleftharpoons> Context and
+  "_Has_type" \<rightleftharpoons> Has_type and
+  "_Lam" \<rightleftharpoons> Abs and
+  "_Pi" "_arrow" \<rightleftharpoons> Prod
 translations
   "_Trueprop(G, t)" \<rightleftharpoons> "CONST Trueprop(G, t)"
   ("prop") "x:X" \<rightleftharpoons> ("prop") "\<turnstile> x:X"
@@ -52,13 +59,6 @@
   [(\<^const_syntax>\<open>Prod\<close>,
     fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\<open>_Pi\<close>, \<^syntax_const>\<open>_arrow\<close>))]
 \<close>
-syntax_consts
-  "_Trueprop" \<rightleftharpoons> Trueprop and
-  "_MT_context" \<rightleftharpoons> MT_context and
-  "_Context" \<rightleftharpoons> Context and
-  "_Has_type" \<rightleftharpoons> Has_type and
-  "_Lam" \<rightleftharpoons> Abs and
-  "_Pi" "_arrow" \<rightleftharpoons> Prod
 
 axiomatization where
   s_b: "*: \<box>"  and
diff -r be8c0e039a5e -r bc936d3d8b45 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/FOL/IFOL.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -102,8 +102,8 @@
   where \<open>x \<noteq> y \<equiv> \<not> (x = y)\<close>
 
 syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o"  ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
+syntax_consts "_Uniq" \<rightleftharpoons> Uniq
 translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
-syntax_consts "_Uniq" \<rightleftharpoons> Uniq
 
 print_translation \<open>
  [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
@@ -747,10 +747,10 @@
   ""            :: \<open>letbind => letbinds\<close>              (\<open>_\<close>)
   "_binds"      :: \<open>[letbind, letbinds] => letbinds\<close>  (\<open>_;/ _\<close>)
   "_Let"        :: \<open>[letbinds, 'a] => 'a\<close>             (\<open>(let (_)/ in (_))\<close> 10)
+syntax_consts "_Let" \<rightleftharpoons> Let
 translations
   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   "let x = a in e"          == "CONST Let(a, \<lambda>x. e)"
-syntax_consts "_Let" \<rightleftharpoons> Let
 
 lemma LetI:
   assumes \<open>\<And>x. x = t \<Longrightarrow> P(u(x))\<close>
diff -r be8c0e039a5e -r bc936d3d8b45 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/Bin.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -117,10 +117,11 @@
   "_Int" :: "num_token \<Rightarrow> i"  (\<open>#_\<close> 1000)
   "_Neg_Int" :: "num_token \<Rightarrow> i"  (\<open>#-_\<close> 1000)
 
+syntax_consts
+  "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of
+
 ML_file \<open>Tools/numeral_syntax.ML\<close>
 
-syntax_consts
-  "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of
 
 declare bin.intros [simp,TC]
 
diff -r be8c0e039a5e -r bc936d3d8b45 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -75,9 +75,9 @@
 
 syntax
   "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{# _ \<in> _./ _#})\<close>)
+syntax_consts "_MColl" \<rightleftharpoons> MCollect
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
-syntax_consts "_MColl" \<rightleftharpoons> MCollect
 
   (* multiset orderings *)
 
diff -r be8c0e039a5e -r bc936d3d8b45 src/ZF/List.thy
--- a/src/ZF/List.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/List.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -17,11 +17,11 @@
 syntax
  "_Nil" :: i  (\<open>[]\<close>)
  "_List" :: "is \<Rightarrow> i"  (\<open>[(_)]\<close>)
+syntax_consts "_List" \<rightleftharpoons> Cons
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"
   "[]"          == "CONST Nil"
-syntax_consts "_List" \<rightleftharpoons> Cons
 
 consts
   length :: "i\<Rightarrow>i"
diff -r be8c0e039a5e -r bc936d3d8b45 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/OrdQuant.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -26,14 +26,14 @@
   "_oall"     :: "[idt, i, o] \<Rightarrow> o"        (\<open>(3\<forall>_<_./ _)\<close> 10)
   "_oex"      :: "[idt, i, o] \<Rightarrow> o"        (\<open>(3\<exists>_<_./ _)\<close> 10)
   "_OUNION"   :: "[idt, i, i] \<Rightarrow> i"        (\<open>(3\<Union>_<_./ _)\<close> 10)
+syntax_consts
+  "_oall" \<rightleftharpoons> oall and
+  "_oex" \<rightleftharpoons> oex and
+  "_OUNION" \<rightleftharpoons> OUnion
 translations
   "\<forall>x<a. P" \<rightleftharpoons> "CONST oall(a, \<lambda>x. P)"
   "\<exists>x<a. P" \<rightleftharpoons> "CONST oex(a, \<lambda>x. P)"
   "\<Union>x<a. B" \<rightleftharpoons> "CONST OUnion(a, \<lambda>x. B)"
-syntax_consts
-  "_oall" \<rightleftharpoons> oall and
-  "_oex" \<rightleftharpoons> oex and
-  "_OUNION" \<rightleftharpoons> OUnion
 
 
 subsubsection \<open>simplification of the new quantifiers\<close>
@@ -198,12 +198,12 @@
 syntax
   "_rall"     :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o"        (\<open>(3\<forall>_[_]./ _)\<close> 10)
   "_rex"      :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o"        (\<open>(3\<exists>_[_]./ _)\<close> 10)
+syntax_consts
+  "_rall" \<rightleftharpoons> rall and
+  "_rex" \<rightleftharpoons> rex
 translations
   "\<forall>x[M]. P" \<rightleftharpoons> "CONST rall(M, \<lambda>x. P)"
   "\<exists>x[M]. P" \<rightleftharpoons> "CONST rex(M, \<lambda>x. P)"
-syntax_consts
-  "_rall" \<rightleftharpoons> rall and
-  "_rex" \<rightleftharpoons> rex
 
 
 subsubsection\<open>Relativized universal quantifier\<close>
diff -r be8c0e039a5e -r bc936d3d8b45 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
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>
diff -r be8c0e039a5e -r bc936d3d8b45 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -38,12 +38,12 @@
 syntax
   "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(3\<forall>_\<in>_./ _)\<close> 10)
   "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(3\<exists>_\<in>_./ _)\<close> 10)
+syntax_consts
+  "_Ball" \<rightleftharpoons> Ball and
+  "_Bex" \<rightleftharpoons> Bex
 translations
   "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
   "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
-syntax_consts
-  "_Ball" \<rightleftharpoons> Ball and
-  "_Bex" \<rightleftharpoons> Bex
 
 
 subsection \<open>Variations on Replacement\<close>
@@ -56,10 +56,10 @@
 
 syntax
   "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i"  (\<open>(1{_ ./ _ \<in> _, _})\<close>)
+syntax_consts
+  "_Replace" \<rightleftharpoons> Replace
 translations
   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
-syntax_consts
-  "_Replace" \<rightleftharpoons> Replace
 
 
 (* Functional form of replacement -- analgous to ML's map functional *)
@@ -69,10 +69,10 @@
 
 syntax
   "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i"  (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51])
+syntax_consts
+  "_RepFun" \<rightleftharpoons> RepFun
 translations
   "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
-syntax_consts
-  "_RepFun" \<rightleftharpoons> RepFun
 
 (* Separation and Pairing can be derived from the Replacement
    and Powerset Axioms using the following definitions. *)
@@ -81,10 +81,10 @@
 
 syntax
   "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(1{_ \<in> _ ./ _})\<close>)
+syntax_consts
+  "_Collect" \<rightleftharpoons> Collect
 translations
   "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
-syntax_consts
-  "_Collect" \<rightleftharpoons> Collect
 
 
 subsection \<open>General union and intersection\<close>
@@ -95,12 +95,12 @@
 syntax
   "_UNION" :: "[pttrn, i, i] \<Rightarrow> i"  (\<open>(3\<Union>_\<in>_./ _)\<close> 10)
   "_INTER" :: "[pttrn, i, i] \<Rightarrow> i"  (\<open>(3\<Inter>_\<in>_./ _)\<close> 10)
+syntax_consts
+  "_UNION" == Union and
+  "_INTER" == Inter
 translations
   "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
   "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
-syntax_consts
-  "_UNION" == Union and
-  "_INTER" == Inter
 
 
 subsection \<open>Finite sets and binary operations\<close>
@@ -134,11 +134,11 @@
   "" :: "i \<Rightarrow> is"  (\<open>_\<close>)
   "_Enum" :: "[i, is] \<Rightarrow> is"  (\<open>_,/ _\<close>)
   "_Finset" :: "is \<Rightarrow> i"  (\<open>{(_)}\<close>)
+syntax_consts
+  "_Finset" == cons
 translations
   "{x, xs}" == "CONST cons(x, {xs})"
   "{x}" == "CONST cons(x, 0)"
-syntax_consts
-  "_Finset" == cons
 
 
 subsection \<open>Axioms\<close>
@@ -199,14 +199,14 @@
   ""          :: "pttrn \<Rightarrow> patterns"         (\<open>_\<close>)
   "_patterns" :: "[pttrn, patterns] \<Rightarrow> patterns"  (\<open>_,/_\<close>)
   "_Tuple"    :: "[i, is] \<Rightarrow> i"              (\<open>\<langle>(_,/ _)\<rangle>\<close>)
+syntax_consts
+  "_pattern" "_patterns" == split and
+  "_Tuple" == Pair
 translations
   "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
   "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
   "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
-syntax_consts
-  "_pattern" "_patterns" == split and
-  "_Tuple" == Pair
 
 definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   where "Sigma(A,B) \<equiv> \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
@@ -268,14 +268,14 @@
   "_PROD"     :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3\<Prod>_\<in>_./ _)\<close> 10)
   "_SUM"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3\<Sum>_\<in>_./ _)\<close> 10)
   "_lam"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3\<lambda>_\<in>_./ _)\<close> 10)
+syntax_consts
+  "_PROD" == Pi and
+  "_SUM" == Sigma and
+  "_lam" == Lambda
 translations
   "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
   "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
   "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
-syntax_consts
-  "_PROD" == Pi and
-  "_SUM" == Sigma and
-  "_lam" == Lambda
 
 
 subsection \<open>ASCII syntax\<close>
diff -r be8c0e039a5e -r bc936d3d8b45 src/ZF/func.thy
--- a/src/ZF/func.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/func.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -452,10 +452,10 @@
   ""            :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
   "_updbinds"   :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
   "_Update"     :: "[i, updbinds] \<Rightarrow> i"              (\<open>_/'((_)')\<close> [900,0] 900)
+syntax_consts "_Update" "_updbind" \<rightleftharpoons> update
 translations
   "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
   "f(x:=y)"                       == "CONST update(f,x,y)"
-syntax_consts "_Update" "_updbind" \<rightleftharpoons> update
 
 lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)"
 apply (simp add: update_def)