[isabelle] "Bad theory import" for conflicting theory names



When trying to load a theory Fun.thy with the following contents,

  theory Fun
    imports "~~/src/HOL/Library/Multiset"
  (* error: Bad theory import "Multiset" *)
  begin
  end

we get the indicated "Bad theory import" error message. Typically that
error indicates a wrong theory path, but in fact the path is correct
and the real problem is that the Multiset theory transitively depends
on a theory called Fun, and Isabelle(/Pure?) does not support having
multiple theories of the same name.

It would be helpful if the error message pointed out the conflicting
theory names.

Incidentally, if the Multiset theory is already loaded, the error
message changes to "Cannot update finished theory "Fun"" which is much
more helpful.

Cheers,

Bertram




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