Don't emit definition bindings for enumerated constants.

Fixes #78.

This commit also

* fixes uses of constructor definitions (the equations are still
present under the "number2<ty>_thm" name)
* provides a regression test
* a bug fix claim in the release notes.