diff -r 66893c47500d -r 701912f5645a src/ZF/func.thy
--- a/src/ZF/func.thy	Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/func.thy	Fri Aug 23 23:14:39 2024 +0200
@@ -448,18 +448,14 @@
 nonterminal updbinds and updbind
 
 syntax
-
-  (* Let expressions *)
-
   "_updbind"    :: "[i, i] \<Rightarrow> updbind"               (\<open>(2_ :=/ _)\<close>)
   ""            :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
   "_updbinds"   :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
   "_Update"     :: "[i, updbinds] \<Rightarrow> i"              (\<open>_/'((_)')\<close> [900,0] 900)
-
 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)