diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Fun.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -846,6 +846,9 @@
   "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" ("_,/ _")
   "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            ("_/'((_)')" [1000, 0] 900)
 
+syntax_consts
+  "_updbind" "_updbinds" "_Update" \<rightleftharpoons> fun_upd
+
 translations
   "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
   "f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"