misc theory shouldn't define constants

If `misc` defines constants, you have to have its grammar in scope to see them cleanly (the alternative is having to write `misc$constname`). But if you do that, you also bring in everything else that `misc` imports, which is pretty well all of HOL (theories of the reals, integers, floating-point numbers, paths, bags, lazy lists, *etc*).

This is disastrous for isolation of concerns.