src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Fun.thy	Tue Oct 01 20:39:16 2024 +0200
@@ -846,9 +846,6 @@
   "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
   "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            (\<open>_/'((2_)')\<close> [1000, 0] 900)
 
-syntax_consts
-  fun_upd
-
 translations
   "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
   "f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"