1.1 --- a/src/Tools/Code/code_ml.ML Thu Aug 26 14:04:13 2010 +0200
1.2 +++ b/src/Tools/Code/code_ml.ML Thu Aug 26 20:14:24 2010 +0200
1.3 @@ -946,8 +946,8 @@
1.4 (** for instrumentalization **)
1.5
1.6 fun evaluation_code_of thy target struct_name =
1.7 - Code_Target.serialize_custom thy (target, fn _ => fn [] =>
1.8 - serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
1.9 + Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
1.10 + serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
1.11
1.12
1.13 (** Isar setup **)
2.1 --- a/src/Tools/Code/code_target.ML Thu Aug 26 14:04:13 2010 +0200
2.2 +++ b/src/Tools/Code/code_target.ML Thu Aug 26 20:14:24 2010 +0200
2.3 @@ -28,7 +28,7 @@
2.4 -> 'a -> serialization
2.5 val serialize: theory -> string -> int option -> string option -> Token.T list
2.6 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
2.7 - val serialize_custom: theory -> string * serializer
2.8 + val serialize_custom: theory -> string * serializer -> string option
2.9 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
2.10 val the_literals: theory -> string -> literals
2.11 val export: serialization -> unit
2.12 @@ -348,8 +348,8 @@
2.13 else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
2.14 end;
2.15
2.16 -fun serialize_custom thy (target_name, seri) naming program names =
2.17 - mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
2.18 +fun serialize_custom thy (target_name, seri) module_name naming program names =
2.19 + mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
2.20 |> the;
2.21
2.22 end; (* local *)