[isabelle-dev] Locale interpretation with mixins

[Tjark Weber]

On Fri, 2012-09-07 at 17:20 +0200, Makarius wrote:
> So when the code generator sees an interpreted function application
> "loc.c t1 t2 t3 x y z" it should somehow do the right thing, in taking it as 
> "(loc.c t1 t2 t3) x y z", and considering the inner part as "atomic 
> entity" (and instance of c defined earlier in the abstract context).

I recently asked (somewhat clumsily, and not in the context of code
generation) about essentially the same issue:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00218.html

So this is not restricted to code generation or simplification, but
(unsurprisingly) also shows up in other applications. When there is a
recommended way of doing the right thing here, I'd be grateful for a
pointer.

Best regards,
Tjark