# HG changeset patch
# User haftmann
# Date 1282846464 -7200
# Node ID 3b4d63ab03c49de777d5452b5e21d39a2070e935
# Parent  3865cbe5d2be2456ee579a40ce6fd7c393091c62
proper passing of optional module name

diff -r 3865cbe5d2be -r 3b4d63ab03c4 src/Tools/Code/code_ml.ML
--- 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 **)
diff -r 3865cbe5d2be -r 3b4d63ab03c4 src/Tools/Code/code_target.ML
--- 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 *)