Josef: >to shadow the "ML type thm" in the rest of code, Sorry, I maybe don't really understand what you mean by "shadowing" here. You can define another type "thm" and hope the user will miss this attempt at cheating. But again, that's not something that will happen by accident. It will not be a bug, but a conscious cheat. Freek