# [isabelle] problem with locales

I have the following two locales:
locale node =
fixes nil :: "'node"
assumes infinite: "¬ finite (UNIV::'node set)"
begin
definition "domain f = {x :: 'node . - (f x = (nil::'node))}"
end
locale list = node +
fixes "next" :: "'node => 'node"
fixes val :: "'node => 'node"
assumes "next (nil::'node) = nil"
These locales generate error "Type unification failed". If I drop the
definition from the first locale then I do not get this message.
More generally. Is there a standard mechanism to enforce
the type 'node from the first locale to be the same as the
type node from the second locale?
Best regards,
Viorel

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*