[isabelle-dev] AFP/JinjaThreads failure

[Makarius]

On Tue, 10 Apr 2012, Brian Huffman wrote:

> On Tue, Apr 10, 2012 at 3:06 PM, Makarius <makarius at sketis.net> wrote:
>> Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error:
>>
>> *** No code equations for one_word_inst.one_word
>> *** At command "by" (line 174 of
>> "afp-devel/thys/JinjaThreads/Common/BinOp.thy")
>>
>> What needs to be done here?
>
> This is probably related to my changeset Isabelle/9475d524bafb, where
> I redefined a bunch of word operations with lift_definition instead of
> definition.
>
> I guess the quick fix would be to declare some extra code equations
> manually. The proper fix would be to figure out exactly how and when
> the lift_definition command should declare code equations
> automatically.

This issue is still open.  Who feels resonsible to fix it?  Brian or 
Andreas Lochbihler himself?

Gerwin normally allocates 1 or 2 weeks after an Isabelle release to 
finalize stable AFP, but if the above requires further changes to Isabelle 
than it is too late.


 	Makarius