Thanks Florian, it helps. It is apparently the same issue as with typerep. I fixed it.
Amine. Florian Haftmann wrote: > Hi Amine, > > >> *** Clash of specifications "Sign.sign.size_sign_inst.size_sign_def" and >> "Sign.sign.size_sign_inst.size_sign_def" for constant "Nat.size_class.size" >> *** At command "theory". >> > > I guess that you have a theory which introduces a type "sign". When you > ensure that this theory has "Plain" as ancestor, the problem should > disappear; if not, I think I'll have a look at the offending theories. > > Hope this helps, > Florian > >
