Introducing lets also might solve another problem, the fact that now, by eta-expansion and combinator lifting, too many functions are introduced.
(Argh, it might make local computations explicit, but at the expense of introducing local variables instead of function arguments.)
I tried a few forms, they all look wrong. Problem is that in the translation scheme used, a let v = e0 in e1 is inversed into a series of thunks where e1 is set up first, v refers to a position in that thunk, and e0 is reduced before e1 is reduced. The whole let thing just seems superfluous and upside-down/inside-out.
032910: Introducing lets is done, it just boils down to an old observation that the DOT representation is somewhat more convenient then ANF, but I went for ANF, since that's somewhat better readable and better known anyway.
033010: And now I am annoyed again, the lets don't play nice with the direct coding scheme I had.