5.1r) Instantiating an already declared type
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.
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?