It is not clear to me whether the original was printing
incorrectly (since we did not have the TopLevel flag before now), or
if this behaviour is expected.

For the time being I am assuming the former.