Any update on this?
The translator interprets
if (...) call f(...) ; return
as if it were
if (...) { call f(...) ; return }
This has been added to the list of known bugs (in the file tlatools/src/pcal/trans.java in the Codeplex repository). None of those bugs has a high priority, so I don't know when any of them will be fixed.
Leslie