[isabelle-dev] unbound Code.add_type_cmd
bulwahn at in.tum.de
Wed Sep 7 10:30:43 CEST 2011
Changesets f523923d8182 and 3bc39cfe27fe should have resolved the issue.
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 code generator invocations by
> generic code generator invocations to enable the long-term removal of
> the SML code generator.
> I agree, Florian knows probably best how to resolve this issue easy
> and clean.
> In the long run, we are planning to get rid of Executable_Set and
> add_type_cmd anyway by providing data refinement within the logic
> (and/or the current efforts towards a own set type).
> On 08/29/2011 04:37 PM, Makarius wrote:
>> For quite some time isatest produces the following error with SML/NJ:
>> Loading theory "Executable_Set"
>> *** Error in
>> *** <instream>:2.3-2.20 Error: unbound variable or constructor:
>> add_type_cmd in path Code.add_type_cmd
>> *** At command "setup" (line 25 of
>> This is because SML/NJ does not have managed ML names spaces within
>> the theory context as Poly/ML. So any overriding of structure Code
>> on the toplevel stays persistent. The conflict is caused by the code
>> generator itself: it provides a static structure Code (in
>> ~~/src/Pure/Isar/code.ML), and uses the same name to wrap up
>> generated code in certain situations. Grepping for "Code" in the
>> sources reveals some such places.
>> Florian probably knows best how to avoid this overlap.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev