Revised version without functional changes.