Re: [isabelle-dev] unbound Code.add_type_cmd

2011-09-07 Thread Florian Haftmann
> Changesets f523923d8182 and 3bc39cfe27fe should have resolved the issue. Thanks a lot, I have overlooked the other occurence. I suggest to move the symbolic name identifier to code_target and reference it uniformly from all ocurrences. Florian -- Home: http://www.in.tum.de/~haftmann

[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-09-07 Thread Florian Haftmann
Hi all, again a report about the current affairs: a) state of discussion IMHO I view the discussion at the point that we want 'a set back after the next release. As a consequence, developers are cordially invited to figure out remaining problems involving their contributions to the system, or sc

Re: [isabelle-dev] unbound Code.add_type_cmd

2011-09-07 Thread Lukas Bulwahn
Changesets f523923d8182 and 3bc39cfe27fe should have resolved the issue. Lukas On 09/02/2011 11:40 AM, Lukas Bulwahn wrote: The reason that this issue has just recently become apparent, is due to changes 322d1657c40c ff. by Andreas Lochbihler. He assisted in replacing (Stefan Berghofer's) SML