There are actually several affected functions: Discrete.sqrt size_fset lapprox_posrat size_multiset set_encode card_UNIV_fun card_UNIV_set card_UNIV_finfun
I have no idea what causes this and why my changed affected it. I also do not have the faintest idea what I could possibly do to fix it. I also do not understand why "export_code … checking" puts everything in a single module and if that perhaps has anything to do with it. If I simply do "export_code" (without "checking" and "module_name"), the problem does /not/ occur. (another completely different problem occurs, something about implicits and Typereps)
From what I have seen so far, it seems like there are some lingering issues with code generation in general and Codegenerator_Test in particular that my rather innocuous change exposed, and that simply deleting that one code equation that I added is not the solution we want (not even in the short term).
Moreover, at least one AFP entry (namely Rene Thiemann's Algebraic_Numbers) crucially depends on a similar code equation for "binomial", which causes the exact same problem. We could just leave this orphaned code equation in the AFP for now, but that does not strike me as a good solution either.
Cheers, Manuel _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
