At the very very end of section 3, the rule for function call in the target language is goofed up. You don't want the xi's to be used for both the formal parameters of f and the actual arguments. Ah, I see, you wanted rho, f (..., yi, ...) hook v below the line.