[isabelle] problem with locales

I have the following two locales:

locale node =
  fixes nil :: "'node"
  assumes infinite: "¬ finite (UNIV::'node set)"
  definition "domain f = {x :: 'node .  - (f x = (nil::'node))}"

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,


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