[isabelle-dev] unbound Code.add_type_cmd
makarius at sketis.net
Mon Aug 29 16:37:23 CEST 2011
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.
More information about the isabelle-dev