src/Tools/Code/code_target.ML

   val assert_target: theory -> string -> string
   val the_literals: theory -> string -> literals
   type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
   val serialization: (int -> Path.T option -> 'a -> unit)
-    -> (string list -> int -> 'a -> string * string option list)
+    -> (string list -> int -> 'a -> string * (string -> string option))
     -> 'a -> serialization
   val set_default_code_width: int -> theory -> theory
 
   val allow_abort: string -> theory -> theory
   type tyco_syntax = Code_Printer.tyco_syntax

 
 
 (** abstract nonsense **)
 
 datatype destination = Export of Path.T option | Produce | Present of string list;
-type serialization = int -> destination -> (string * string option list) option;
+type serialization = int -> destination -> (string * (string -> string option)) option;
 
 fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
   | serialization _ string content width Produce = SOME (string [] width content)
   | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content);
 

 
 fun export_code_for thy some_path target some_width some_module_name args naming program names =
   export some_path (mount_serializer thy target some_width some_module_name args naming program names);
 
 fun produce_code_for thy target some_width module_name args naming program names =
-  produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
+  let
+    val (s, deresolve) = produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names)
+  in (s, map deresolve names) end;
 
 fun present_code_for thy target some_width module_name args naming program (names, selects) =
   present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
 
 fun check_code_for thy target strict args naming program names_cs =