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
