Hi Lucas, perhaps the source of the confusion can be found here:
http://isabelle.in.tum.de/repos/isabelle/file/6b31b143f18b/src/Pure/codegen.ML I.e. due to a misunderstanding of interfacing convention (0 is also a valid size), Codegn.test_term in Isabelle2009 would increase its size argument by 1, which should not happen. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 260 bytes Desc: OpenPGP digital signature URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090922/f21d2e46/attachment.pgp>