diff -r 7e1b66416b7f -r ed264056f5dc src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/HOL.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -233,6 +233,10 @@
   where "Let s f \<equiv> f s"
 
 nonterminal letbinds and letbind
+
+open_bundle let_syntax
+begin
+
 syntax
   "_bind"       :: "[pttrn, 'a] \<Rightarrow> letbind"              (\<open>(\<open>indent=2 notation=\<open>mixfix let binding\<close>\<close>_ =/ _)\<close> 10)
   ""            :: "letbind \<Rightarrow> letbinds"                 (\<open>_\<close>)
@@ -244,6 +248,8 @@
   "_Let (_binds b bs) e"  \<rightleftharpoons> "_Let b (_Let bs e)"
   "let x = a in e"        \<rightleftharpoons> "CONST Let a (\<lambda>x. e)"
 
+end
+
 axiomatization undefined :: 'a
 
 class default = fixes default :: 'a