[isabelle-dev] Regression in the sublocale command

[Clemens Ballarin]

On 14 February, 2015 10:11 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: 
 
> I guess you found out using bisection.  But I read some incertainty in
> your words »appears to have been introduced«.  Is the changeset
> 8fab871a2a6f a reliable entrance point or a first approximation?

That particular problem is present in 8fab871a2a6f but not its parent (but who knows how often that behaviour changed in the history?)  It looks like there are more of these kinds of problems lurking, but unfortunately, I no longer fully understand the code, so I will have to rely on your help.  In particular, I would like to know what went wrong here.

Clemens