I thought it would be good to clarify my position in a shorter email: The automatically-generated typerep instances work fine on typedef or datatype commands, where the instance resides in the same theory as the type definition.
It is also OK if instances are generated *within Typerep.thy* for all types defined in earlier theories. However, if the merging of two theories causes a typerep instance to be generated, this is *very bad*. As far as I can tell, Florian would not necessarily disagree with this. His advice to Amine, recommending to contort his theory dependencies, has the effect of avoiding theory merges which would cause typerep instances to be generated. My advice is to simply disable theory-merge instance generation. This would be much better than the current workaround, which relies on carefully preventing this feature from ever being exercised. If, during a theory merge, the typerep package noticed a missing instance, printing an error message would actually be more helpful than the current behavior. - Brian
