[isabelle-dev] isabelle test failures

[Lukas Bulwahn]

I bisected the failure further on my local machine and it turns out it 
is related to the changeset

changeset:   46143:463b594e186a
user:        wenzelm
date:        Fri Jan 06 20:18:49 2012 +0100
summary:     refined case syntax again, improved treatment of 
constructors without arguments, e.g. "case a of (True, x) => x";


Lukas

On 01/11/2012 09:16 AM, Lukas Bulwahn wrote:
> Hi all,
>
>
> the latest failures of the isabelle test of the form:
>
> /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs:XXXX:XX: 
>
>     Conflicting definitions for `ad'
>     Bound at: 
> /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs:XXXX:XX-XX
>               
> /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs:XXXX:XX-XX
>     In a case alternative
>
>
> causing quickcheck to fail in ex/Tree23.thy is not related to any 
> modifications in quickcheck, but is probably related to some recent 
> changes in the code generator or some setup on macbroy21.
>
>
> Lukas
>
>
>