diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/ZF/func.thy
--- a/src/ZF/func.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/ZF/func.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -452,7 +452,8 @@
   ""            :: "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
+syntax_consts
+  update
 translations
   "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
   "f(x:=y)"                       == "CONST update(f,x,y)"