diff -r 7e1b66416b7f -r ed264056f5dc src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/Fun.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -840,6 +840,9 @@
 
 nonterminal updbinds and updbind
 
+open_bundle update_syntax
+begin
+
 syntax
   "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind"             (\<open>(\<open>indent=2 notation=\<open>mixfix update\<close>\<close>_ :=/ _)\<close>)
   ""         :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
@@ -852,6 +855,8 @@
   "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
   "f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"
 
+end
+
 (* Hint: to define the sum of two functions (or maps), use case_sum.
          A nice infix syntax could be defined by
 notation