[isabelle-dev] AFP http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/563de86630d9

[Lukas Bulwahn]

On 10/13/2011 10:52 AM, Florian Haftmann wrote:
> Hi Lukas,
>
> »removing checking of generated code because it fails on the mira
> testing infrastructure due to a missing Pure image« – I don't quite
> understand this.  Why exactly is the check failing?
>
> 	Florian
>
The issue can be observed at

http://isabelle.in.tum.de/reports/Isabelle/report/5497697969e943bda524c4b01be7d12e

Checking that the generated code in the Depth-First-Search AFP entry 
actually compiles with ML is a minor point anyway, so I did not dig into 
the details, but removed the check instead.


Lukas