On Fri, 11 Oct 2013, David Matthews wrote:
I've fixed this and another bug that appeared when I disabled the optimisation that was causing the problem. I've ported the fixes to the fixes branch. I'm a bit concerned about this because it's clearly generating incorrect code. Should there perhaps be another release fairly soon?
As you know the official release of Isabelle2013-1 is in the pipeline. Right now Isabelle2013-1-RC3 bundles Poly/ML 5.5.1 without any of the recent fixes. I don't mind to revert to Poly/ML 5.5.0 for the final Isabelle release, so you don't have to rush anything here.
I am on vacation from 17-Oct-2013 to 04-Nov-2013, which means I will be unavailable for the usual tests with Isabelle and AFP on all reachable platforms.
Makarius