[isabelle-dev] Duplicate theory??

[Lawrence Paulson]

I’m trying to install some material in time for the next release and I've got tangled up in some issue connected with session structure. The theory header looks like this:

theory "Free_Abelian_Groups"
  imports
    Product_Groups
    "HOL-Cardinals.Cardinal_Arithmetic"
    "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence”

But any attempt to load it produces the error message

> /Users/lp15/isabelle/Repos/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
> Cannot start: 
> *** Duplicate theory "HOL-Cardinals.Cardinal_Arithmetic" vs. "/Users/lp15/isabelle/Repos/src/HOL/Cardinals/Cardinal_Arithmetic.thy”

I note that absolutely nothing in the distribution imports HOL-Cardinals. However, it’s imported in a number of places in the AFP. What gives?
Larry