--- a/src/FOL/IFOL.thy Sun Sep 29 21:40:37 2024 +0200
+++ b/src/FOL/IFOL.thy Sun Sep 29 21:57:47 2024 +0200
@@ -747,7 +747,8 @@
"" :: \<open>letbind => letbinds\<close> (\<open>_\<close>)
"_binds" :: \<open>[letbind, letbinds] => letbinds\<close> (\<open>_;/ _\<close>)
"_Let" :: \<open>[letbinds, 'a] => 'a\<close> (\<open>(\<open>notation=\<open>mixfix let in\<close>\<close>let (_)/ in (_))\<close> 10)
-syntax_consts "_Let" \<rightleftharpoons> Let
+syntax_consts
+ Let
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
"let x = a in e" == "CONST Let(a, \<lambda>x. e)"