diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -46,6 +46,11 @@
   "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
   "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
 
+syntax_consts
+  "_do_block" "_do_cons" \<rightleftharpoons> bind_do and
+  "_do_bind" "_thenM" \<rightleftharpoons> bind and
+  "_do_let" \<rightleftharpoons> Let
+
 translations
   "_do_block (_do_cons (_do_then t) (_do_final e))"
     \<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"