[isabelle-dev] unbound Code.add_type_cmd

[Lukas Bulwahn]

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).

Lukas


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 
> /mnt/home/isatest/isadist/Isabelle_29-Aug-2011/src/HOL/Library/Executable_Set.thy
> *** <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 
> "/mnt/home/isatest/isadist/Isabelle_29-Aug-2011/src/HOL/Library/E
>
> 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.
>
>
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>