Hi Stephan,
You can constrain foo's type to 'a in loc2 as follows:
locale loc2 = loc +
fixes a_set :: "'a set"
constrains foo :: "'a"
begin
Alternatively, you can redeclare foo explicitly:
locale loc2 = loc foo
for foo :: "'a" +
fixes a_set :: "'a set"
begin

`The second solution would erase all mixfix syntax for foo if there was
``any.
`

`Since type classes must mention exactly one type type variable, so
``Isabelle unifies the type variables, but locales do not have this
``restriction.
`
Hope this helps,
Andreas
Am 16.01.2012 14:57, schrieb Stephan van Staden:

`Hi, I'm running into a problem whose solution should be simple. The
``following is
`fine:
class cla = fixes foo :: "'a"
class cla2 = cla + fixes a_set :: "'a set"
begin
lemma lem1: "foo \<in> a_set \<Longrightarrow> true"
sorry
end
Yet what I want is not fine:
locale loc = fixes foo :: "'a"
locale loc2 = loc + fixes a_set :: "'a set"
begin
lemma lem1: "foo \<in> a_set \<Longrightarrow> true"
sorry
end
The error I get is:
Type unification failed
Type error in application: incompatible operand type
Operator: op ∈ foo :: ('b ⇒ bool) ⇒ bool
Operand: a_set :: 'a ⇒ bool

`Can I somehow tell Isabelle that I want the type of a_set to be
``"'a::loc set"?
`
Thanks in advance for help!