Error defining dataype in Isabelle -

i'm working on theory uses topology , helpful have type of open sets. tried following:

    context topology begin typedef openset = "{u. u ∈ t}" end 

where topology locale , context command correctly gives output

locale topology =   fixes t :: "'a set set"    assumes "topology t" 

however, following error:

extra type variables in representing set: "'a" error(s) above occurred in typedef "openset"

what mean? here t set of sets , want have type consisting of sets belonging t, there way can done?

first of all, not data type – ‘normal’ type definition.

the problem cannot have type definitions depend on locale parameters. logical foundations of isabelle not permit such thing @ moment. cf. question: what kind of type definitions legal in local contexts?