diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Fun.thy	Tue May 23 21:43:36 2023 +0200
@@ -1353,7 +1353,7 @@
 
 text \<open>Simplify terms of the form \<open>f(\<dots>,x:=y,\<dots>,x:=z,\<dots>)\<close> to \<open>f(\<dots>,x:=z,\<dots>)\<close>\<close>
 
-simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
+simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>
   let
     fun gen_fun_upd NONE T _ _ = NONE
       | gen_fun_upd (SOME f) T x y = SOME (Const (\<^const_name>\<open>fun_upd\<close>, T) $ f $ x $ y)
@@ -1380,7 +1380,7 @@
                 resolve_tac ctxt @{thms ext} 1 THEN
                 simp_tac (put_simpset ss ctxt) 1)))
       end
-  in proc end
+  in K proc end
 \<close>