[isabelle-dev] Unproven class relation finite_lattice_complete < countable

[Tobias Nipkow]

I have just added a new theory Library/Finite_Lattice. It clashes with theory
Library/Countable in a way I don't understand. If you import both

theory Scratch
imports "~~/src/HOL/Library/Finite_Lattice" "~~/src/HOL/Library/Countable"
begin

Isabelle complains

Unproven class relation finite_lattice_complete < countable

Class finite_lattice_complete is defined in Finite_Lattice but I have no idea
why it should be a subclass of countable. Theory Finite_Lattice does not import
Countable but Countable uses class finite.

Is there some general potential problem with classes when merging theories?

Thanks
Tobias