src/Pure/Tools/codegen_serializer.ML

       string list list
       -> OuterParse.token list ->
       ((string -> string option)
         * (string -> CodegenThingol.itype pretty_syntax option)
         * (string -> CodegenThingol.iexpr pretty_syntax option)
-      -> string list option
+      -> string list * string list option
       -> CodegenThingol.module -> unit)
       * OuterParse.token list;
   val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
     ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
   val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax;

     string list list
     -> OuterParse.token list ->
     ((string -> string option)
       * (string -> itype pretty_syntax option)
       * (string -> iexpr pretty_syntax option)
-    -> string list option
+    -> string list * string list option
     -> CodegenThingol.module -> unit)
     * OuterParse.token list;
 
 fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
     postprocess (class_syntax, tyco_syntax, const_syntax)
-    select module =
+    (drop: string list, select) module =
   let
     fun from_module' resolv imps ((name_qual, name), defs) =
       from_module resolv imps ((name_qual, name), defs)
       |> postprocess (resolv name_qual);
   in

             ml_from_expr NOBR e
           ]
       | ml_from_expr fxy (INum (n, _)) =
           brackify BR [
             (str o IntInf.toString) n,
-            str ":IntInf.int"
+            str ":",
+            str "IntInf.int"
           ]
       | ml_from_expr _ (IChar (c, _)) =
           (str o prefix "#" o quote)
             (let val i = (Char.ord o the o Char.fromString) c
               in if i < 32 

                parse_multi_file
                  (K o SOME o str o suffix ";" o prefix "val _ = use "
                   o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer
             | _ => Scan.fail ());
   in
-    (parse_multi
-     || parse_internal serializer
-     || parse_single_file serializer)
-    >> (fn seri => fn (class_syntax, tyco_syntax, const_syntax) => seri 
-         (class_syntax, tyco_syntax, const_syntax))
+    parse_multi
+    || parse_internal serializer
+    || parse_single_file serializer
   end;
 
 fun mk_flat_ml_resolver names =
   let
     val mangler =

       |> Option.map (fst o fst)
       |> the_default 0;
   in
     (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
     #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
-    >> (fn (seri) => fn (class_syntax, tyco_syntax, const_syntax) => seri 
-         (class_syntax, tyco_syntax, const_syntax))
   end;
 
 end; (* local *)