Re: [isabelle] Isabelle2016-1-RC3: problem with records



On 27/11/16 21:34, Florian Haftmann wrote:
> Am 27.11.2016 um 15:24 schrieb Makarius:
>> On 25/11/16 14:15, Thiemann, Rene wrote:
>>>
> A glimpse at the code guides to line record.ML:1586 that explicitly
> mentions that a a' deficiency
> 
> 	val inject_prop =  (* FIXME local x x' *)
> 
> where the comment was added in b5d1873449fb about 5 years ago.
> 
> The code behind seems to date back to 2004.
> 
> This particularly means that such record declarations are likely to
> never have worked properly â and definitely do not produce a proper
> inject rule in Isabelle2016, which I have checked explicitly.
> 
> For the moment I am inclined not to risk a last minute change to that
> ancient record package layer, although the resulting error message is,
> admittedly, cryptic.

Yes, we cannot do anything right now. The record package is lagging
behind many years and still awaiting proper localization.


	Makarius



Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.