[isabelle] Isabelle2014-RC1: defaults for (co)datatype selectors

In Isabelle2013-2, one could declare a selector name that hides another constant.
For example, in the following declaration, the new selector tl hides the constant "List.tl".

codatatype 'a llist = LNil (defaults tl: LNil) | LCons 'a (tl: "'a llist")

In Isabelle2014-RC1, defaults must be specified in a separate where clause, so I tried the following:

codatatype 'a llist = LNil | LCons 'a (tl: "'a llist") where "tl LNil = LNil"

However, this results in a type error, because tl in the where clause is parsed as List.tl. How can I use existing names for selectors with defaults in the new format?


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