[isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode

[Thomas Sewell]

Quoting Alex:

Someone who knows more about records can probably explain why this
declaration isn't issued internally by default...

I suppose everyone is expecting that someone to be me. It's not. The 
record package is huge, and I didn't have a clear idea of all the 
applications it had, so I left as much of the interface as possible 
unchanged. I guess I did remove some inner constants, but they were 
clearly meant to be implementation details.

The 'ext' constant, which constructs the (| a = 1, b = 2 |) style 
syntax, looks like it's been there a while. Assuming this syntax is used 
in the future, it will probably be backed by a constant. Naming it as a 
constructor would seem reasonable, but I have no idea what the 
ramifications would be. I don't know anything at all about the internals 
of the datatype package.

The only concern I can see is a potential performance problem with the 
datatype package - there are some very large records in use. At least 
one, anyway. I did consider at one point adding a flag which would turn 
off some features of the package for users concerned about performance. 
This would make it easier to add new features in if needed.

Yours,
     Thomas.