[isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9

[Makarius]

On 08/12/16 17:41, David Matthews wrote:
> 
> On 08/12/2016 15:01, Florian Haftmann wrote:
>> Hi all,
>>
>> when testing polyml-test-7a7b742897e9 I found out that this breaks
>> session Algebraic_Numbers in the AFP:
>>
>> *** At command "value" (line 42 of
>> "/mnt/home/haftmann/data/tum/afp/devel/thys/Algebraic_Numbers/Algebraic_Number_Tests.thy")
>>
>> *** exception Div raised (line 302 of "./basis/InitialBasis.ML")
>>
>> It looks like a change in the semantics of integer division in PolyML,
>> but this is entirely speculative.
>>
> 
> No, it was a bug in the testing version of Poly/ML.  Thanks for pointing
> it out and in particular including the line number which allowed me to
> see immediately what was wrong.  Hopefully the commit I've just pushed
> will have fixed it.

This works, see
http://isabelle.in.tum.de/repos/isabelle/rev/d23b7c9b9dd4


	Makarius