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



Dear all,

consider the following record definition:

record foo = 
  a :: bool
  a' :: bool

It compiles with Isabelle 2016, but not with Isabelle 2016-RC3.
In the release candidate there is a name clash of internal variables
in the record construction which seem to be generated by just adding
a prime (â):

Duplicate variables on left hand side of equation, in theorem:
equal_foo_ext_inst.equal_foo_ext âa = ?a, a' = ?a', â = ?moreâ âa = ?a', a' = ?a'', â = ?more'â â
?a = ?a' â ?a' = ?a'' â ?more = ?more'
Failed to define record "foo"

Cheers,
RenÃ


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