The naming is now "consistent" in the sense that a transformation
argument is not taken in place of another.

However, it does not solve all the issues related to using
the IDE without the "introduce premises" enabled.