As Andreas and Lars have pointed out, this is the issue described in ยง7.1 in the tutorial on code generation.
I will have a look at this after the release.
Florian
Am 12.01.2016 um 23:51 schrieb Makarius:
> On Tue, 12 Jan 2016, Manuel Eberl wrote:
>
>> I commented out the code equation in question and
>> HOL-Codegenerator_Test runs through again.
>
> Thanks.
>
> For the historical record: that is Isabelle/18a217591310.
>
> (Mercurial changeset ids allow to talk about history in a timeless and
> stateless manner.)
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
