defined at different places in the generated file (in order to avoid
  name clashes, and for clarity).