[isabelle-dev] Regression in the sublocale command

[Florian Haftmann]

> 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.

Can you point me to a source position where you get stuck?  Doing a
short revisitation of the history, I found out that my only change to
the machinery itself has been 54795:e58623a33ba5.  The refinement of the
commands and their integration with local theories happened smoothly on
the surface level, and it should not be that difficult to step through
it after some guidance through the typical indirections of the local
theory interface.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150214/a04110d4/attachment.sig>