[isabelle-dev] Tweak Haskell output for future Haskell compatibility.

[Tobias Nipkow]

Am 08/05/2012 13:49, schrieb Peter Lammich:
> datatype a'::heap linked_list = nil | node 'a "'a linked_list ref"

Actually, I think this does not do what you hope it does, hence the magic is
still in there. But Lukas showed me a related defn:

datatype 'a ref = Ref nat

where 'a is a phantom type but for extra-logical reasons you want to restrict 'a
to some type class. Extra-logical reasons can be quite compelling ;-) I'm convinced.

Tobias