[isabelle-dev] HOL-Codegenerator_Test error

[Makarius]

On Tue, 12 Jan 2016, Manuel Eberl wrote:

> From what I have seen so far, it seems like there are some lingering 
> issues with code generation in general and Codegenerator_Test in 
> particular that my rather innocuous change exposed, and that simply 
> deleting that one code equation that I added is not the solution we want 
> (not even in the short term).

I generally agree that things need to be done right, but for the moment 
(3201ddb00097 and after) the main priority is to get back to a repository 
where "isabelle build -a" works.  There are already several changes pushed 
on top of the bad state, which easily leads into a situation that takes a 
long time to disentangle.

I have myself various changes waiting and cannot move forward now, neither 
on main Isabelle nor AFP.


 	Makarius