[isabelle] code_include SML and eval



Hi all,

I have written some code-generation setup that requires on an additional module. What is the recommended way to include this additional module into the generated code?
I tried:
code_include SML "Foo" {*
 structure Foo = struct
   exception Bar;
 end;
*}

This works fine for code_export.
However, the eval-method seems to have problems with it:
lemma "(5::code_numeral) = Code_Numeral.of_nat 5"
 apply eval
yields:
*** Error (line 3):
*** in expected but structure was found
*** Error (line 3):
*** Expression expected but structure was found
*** Error (line 3):
*** end expected but structure was found
*** Error (line 3):
*** ) expected but structure was found
*** Error (line 3):
*** ) expected but structure was found
*** Exception- ERROR "Static Errors" raised
*** At command "apply".

Without the code_include, it works fine!

How should I include my additional code. And what is code_include good for?

Regards and thanks in advance for any hints,
 Peter








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