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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev