Brian Huffman wrote:
For reasons related to pretty-printing (which, to be honest, I don't completely understand), other developers have determined that opaque ascription should be avoided in the Isabelle sources. So most uses of opaque ascription have now been replaced with "abstype", like this:
structure Bar : Foo = struct abstype T = MkT of int * bool with ... end; end;
But according to what you've said, the following code with "datatype" instead of "abstype" works in exactly the same way:
structure Bar : Foo = struct datatype T = MkT of int * bool ... end;
(and if I understand correctly, the "datatype" and "abstype" versions both work exactly like the original version with "type" and opaque ascription.)
It seems that there is no advantage to using "abstype" over "datatype" in this situation: The only difference of "abstype" is the "with...end" block, which is redundant since "struct...end" already delimits the scope of the declaration.
From the point of view of run-time representation of the values of the datatype there is no difference between an abstype and a datatype and across opaque or transparent signatures. There are differences in the way pretty printing is handled; in particular there were changes between different versions of Poly/ML. Also abstype removes the equality attribute from the datatype. I would imagine that the Isabelle maintainers are attempting to minimise the changes in the code between the different versions of Poly/ML.
Regards, David