Quoting Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de>:
thanks for this offer. But this misperception has not only infected size but all datatype tools using the Datatype_Aux.interpret_construction combinator which assumes exactly the same restriction. Therefore my proposal to internally provide a consolidated view of the datatype specifications with type parameter names made uniform, to handle the issue at one place and not in every datatype package extension separately.
Hi Florian, why can't we repair interpret_construction so that it handles this case properly? Nevertheless, it would be interesting to see what goes wrong, since your example used to work in older releases of Isabelle without further ado. Greetings, Stefan _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
