# [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug

There seems to be a strange dependency between
Efficient_Nat and the import order of totally unrelated theories.
As an example, consider the following theories:
theory A
imports Main
begin
end
theory Scratch
imports
"~~/src/HOL/Library/Efficient_Nat"
"~~/src/HOL/Imperative_HOL/Imperative_HOL"
A
begin
export_code Unity Array.len in Scala_imp file -
Produces:
[...]
def len[A : Heapa.heap](a: collection.mutable.ArraySeq[A]): Unit => Nat =
(b: Unit) =>
{
val (): Unit = b
val i: BigInt = ((_: Unit) => Array.len(a)).apply(());
Nat(i.as_BigInt)
}
[...]
which is a type-error, as Array.len returns a "Natural", not a "BigInt".
However, when removing the import of A, or moving it up, the generated
code correctly becomes:
def len[A : Heapa.heap](a: collection.mutable.ArraySeq[A]): Unit => Nat =
(b: Unit) =>
{
val (): Unit = b
val i: Natural = ((_: Unit) => Array.len(a)).apply(());
Nat(i.as_BigInt)
}
For Scala code generation, this is a real showstopper! Fortunately, this
problem seems not to occur for SML.
What is happening here. Why does the import order wrt an *empty* theory
change the output of the code generator?
And how to fix the problem, which rules for imports do I have to follow
in order to avoid this problem?
Best,
Peter

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*