[isabelle] theory FSet exists twice



Hi list,

Iâm trying to use Nominal2 (as shipped in AFP-2016) in a theory that
also usesÂÂ"~~/src/HOL/Library/FSet". This leads to

exception THEORY raised (line 221 of "context.ML"):
 Duplicate theory name
 {..., BNF_Greatest_Fixpoint, Filter, Main, Conditionally_Complete_Lattices, FSet}
 {..., Quotient_Product, Quotient_Option, Multiset, Quotient_List, FSet}

The problem seems to be that Nominal2_Base imports
"~~/src/HOL/Quotient_Examples/FSet".

Can I work around this problem without modifying HOL or Nominal2?

Also, should the ~~/src/HOL/Quotient_Examples/FSet theory be renamed to
avoid this problem?

Thanks,
Joachim

-- 

Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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