A version of defthmd with testing disabled.
A macro that locally turns off cgen testing and then calls defthmd.
