[isabelle-dev] conflict between code_identifier constant and module_name

[Andreas Lochbihler]

Two months ago, Florian replaced code_module with code_identifier (6646bb548c6b). Now, I 
am having trouble using the greater capabilities of code_identifier. I would like to 
assign a constant to a different module, say

code_identifier constant replicate \<rightharpoonup> (SML) "My_Module.rep"

Then, code generation works fine as long as there is no module_name involved:

definition test where "test = replicate"
export_code test in SML
export_code test in SML module_name foo (* fails due to module dependency cycles *)

Unfortunately, many idioms internally use module_name -- for example, all of the following 
raise errors due to module dependency cycles:

ML {* @{code test} *}
value [code] "test 3 (0 :: nat)"
lemma "test = foo" quickcheck

The same problem also occurs with type constructors. Therefore: What is the intended way 
of using code_identifier with constants?

Best,
Andreas