--- a/src/Tools/Code/code_ml.ML Thu Aug 26 14:04:13 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Aug 26 20:14:24 2010 +0200
@@ -946,8 +946,8 @@
(** for instrumentalization **)
fun evaluation_code_of thy target struct_name =
- Code_Target.serialize_custom thy (target, fn _ => fn [] =>
- serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
+ Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
+ serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
(** Isar setup **)
--- a/src/Tools/Code/code_target.ML Thu Aug 26 14:04:13 2010 +0200
+++ b/src/Tools/Code/code_target.ML Thu Aug 26 20:14:24 2010 +0200
@@ -28,7 +28,7 @@
-> 'a -> serialization
val serialize: theory -> string -> int option -> string option -> Token.T list
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
- val serialize_custom: theory -> string * serializer
+ val serialize_custom: theory -> string * serializer -> string option
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
val the_literals: theory -> string -> literals
val export: serialization -> unit
@@ -348,8 +348,8 @@
else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
end;
-fun serialize_custom thy (target_name, seri) naming program names =
- mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
+fun serialize_custom thy (target_name, seri) module_name naming program names =
+ mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
|> the;
end; (* local *)