avoid relying on "Thm.definitionK" to pick up definitions -- this was an old hack related to locales (to avoid expanding locale constants to their low-level definition) that is no longer necessary
theory Baseimports Mainuses "../../antiquote_setup.ML"beginend