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
Bool = FOL +
types bool 0
arities bool :: term
consts tt,ff :: "bool"
end