merged
authorhaftmann
Thu, 26 Aug 2010 20:14:39 +0200
changeset 38785 afcc1fcb376b
parent 38783 f171050ad3f8 (current diff)
parent 38784 3b4d63ab03c4 (diff)
child 38787 948c002d773b
merged
--- a/src/Tools/Code/code_ml.ML	Thu Aug 26 16:00:54 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Aug 26 20:14:39 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 16:00:54 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Aug 26 20:14:39 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 *)