[isabelle-dev] Duplicate theory??

[Traytel Dmitriy]

> On 8 Apr 2019, at 12:11, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
>> On 7 Apr 2019, at 20:08, Traytel Dmitriy <traytel at inf.ethz.ch> wrote:
>> 
>> In 3a1b2d8c89aa, there is now a bundle cardinal_syntax (and the theory Cardinal_Notations is gone). HOL-Cardinals does not depend on HOL-Library anymore.
> 
> Thanks. But now nothing works. I get
> 
>> /Users/lp15/isabelle/Repos/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
>> Cannot start: 
>> *** Duplicate theory "/Users/lp15/isabelle/Repos/src/HOL/Library/Countable_Set_Type.thy" vs. "HOL-Library.Countable_Set_Type"
> 
> 
> 36821db2e356+ tip

What is the invocation of Isabelle that leads to this? Do you have some local root files?

I have tested as usual with

isabelle build -a

(which succeeded).

Dmitriy