[isabelle-dev] Regression in the sublocale command

[Florian Haftmann]

It appears to be a reading issue.

> sublocale loc1 < x: loc2 A c (* sigma_1 *)
>   where "x.b == B" and "x.d == e" (* tau_1 *)
> sorry
> 
> sublocale loc2 < x: loc1 A b (* sigma_2 *)
>   where "x.c == C" and "x.e == d" (* tau_2 *)
> sorry

Here the second mixin equation already parses as »loc1.e A ≡ loc1.e A«.

Reading apparently takes into account the pre-established rewrite »x.d
== e«.  I am not sure whether this is the intended behaviour.  Anyway,
the »read_with_extended_syntax« using »fold Locale.activate_declarations
deps« has been introduced in eb8b4851b039.

Do you have a Isabelle version at hand where this has worked as desired?

	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/d6c40743/attachment.sig>