>I really don't want to start using complicated module features and functors, for the reasons I explained above. And why is that? Because you really don't want

>I really don't want to start using complicated module features and functors, for the reasons I explained above. And why is that? Because you really don't want to write ML without modules (and you are using them anyway). Edit: Ah, I see, you have an auto-generated ocaml code, which is used along with the Isabelle. That makes sense (although your code generator is rather strange and there is still no need to use lists for memory representations since Isabelle reasoning about memory chunks shouldn't be that hard). Anyway I wouldn't claim that OCaml is that bad for low level programming basing on such a subset of a language.