diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/func.thy
--- a/src/ZF/func.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/func.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -448,10 +448,10 @@
 nonterminal updbinds and updbind
 
 syntax
-  "_updbind"    :: "[i, i] \<Rightarrow> updbind"               (\<open>(\<open>indent=2 notation=\<open>infix update\<close>\<close>_ :=/ _)\<close>)
-  ""            :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
-  "_updbinds"   :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
-  "_Update"     :: "[i, updbinds] \<Rightarrow> i"              (\<open>_/'((_)')\<close> [900,0] 900)
+  "_updbind"    :: "[i, i] \<Rightarrow> updbind"  (\<open>(\<open>indent=2 notation=\<open>infix update\<close>\<close>_ :=/ _)\<close>)
+  ""            :: "updbind \<Rightarrow> updbinds"  (\<open>_\<close>)
+  "_updbinds"   :: "[updbind, updbinds] \<Rightarrow> updbinds"  (\<open>_,/ _\<close>)
+  "_Update"     :: "[i, updbinds] \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>mixfix function update\<close>\<close>_/'((_)'))\<close> [900,0] 900)
 translations
   "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
   "f(x:=y)"                       == "CONST update(f,x,y)"