diff -r 843dba3d307a -r c007e6d9941d src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/FOL/IFOL.thy Tue Oct 01 20:39:16 2024 +0200 @@ -747,8 +747,6 @@ "" :: \letbind => letbinds\ (\_\) "_binds" :: \[letbind, letbinds] => letbinds\ (\_;/ _\) "_Let" :: \[letbinds, 'a] => 'a\ (\(\notation=\mixfix let in\\let (_)/ in (_))\ 10) -syntax_consts - Let translations "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" "let x = a in e" == "CONST Let(a, \x. e)"