In recent mail, I said that I wasn't sure that DEFUNs inside a top-level LET were valid CL. This was a completely error on my part, resulting from my having spent too much time in design discussions to remember how they came out. Yes, it's legal Common Lisp. And the Symbolics implementation supports it correctly, too. Sorry about that.