5.1r) Instantiating an already declared type

[DanielSchoepe]

I think that if one uses the given names Var, Const, etc. for datatypes, tasks 5.1a and 5.1r cannot both be solved. If you declare those types in 1a in the "canonical" way we have seen earlier, they cannot be made concrete later in 5.1r, because they have already been declared. I googled a bit and didn't find a nice solution for this.

One possibility would be to use locales and make Var, Const, etc. type parameters instead. (But then they would appear as 'Var, 'Const, etc., which is not quite what I understand as declaring data types as requested in 1a). Then one could later instantiate those to concrete types.
http://isabelle.in.tum.de/doc/locales.pdf

I found a post to the isabelle ML with the same question, but there were no straight-forward answers:
https://lists.cam.ac.uk/pipermail/cl-is ... 00110.html

How should we handle this? Comment out the solution for 1a and define the concrete types in its place instead to make sure the rest of the file type-checks or should we make Var, Const, etc. type parameters in the relevant functions and predicates, which would lead to a rather convoluted solution?

Cheers,
Daniel