[isabelle-dev] unbound Code.add_type_cmd

[Makarius]

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