src/Pure/Tools/codegen_serializer.ML

       ];
     fun pretty_compact fxy pr [e1, e2] =
       case unfoldr dest_cons e2
        of (es, IConst (c, _)) => (writeln (string_of_int (length es));
             if c = thingol_nil
-            then Pretty.gen_list "," "[" "]" (map (pr NOBR) (e1::es))
+            then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es))
             else pretty_default fxy pr e1 e2)
         | _ => pretty_default fxy pr e1 e2;
   in ((2, 2), pretty_compact) end;
 
 

       | ml_from_type _ (IVarT (v, [])) =
           str ("'" ^ v)
       | ml_from_type _ (IVarT (_, sort)) =
           "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
       | ml_from_type _ (IDictT fs) =
-          Pretty.gen_list "," "{" "}" (
+          Pretty.enum "," "{" "}" (
             map (fn (f, ty) =>
               Pretty.block [str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs
           );
     fun ml_from_pat fxy (ICons ((f, ps), ty)) =
           (case const_syntax f

                   |> cons ((str o resolv) f)
                   |> brackify fxy
                 else
                   ps
                   |> map (ml_from_pat BR)
-                  |> Pretty.gen_list "," "(" ")"
+                  |> Pretty.enum "," "(" ")"
                   |> single
                   |> cons ((str o resolv) f)
                   |> brackify fxy
             | SOME ((i, k), pr) =>
                 if not (i <= length ps andalso length ps <= k)

             :: map (mk_clause "| ") cs
           ) end
       | ml_from_expr fxy (IInst _) =
           error "cannot serialize poly instant to ML"
       | ml_from_expr fxy (IDictE fs) =
-          Pretty.gen_list "," "{" "}" (
+          Pretty.enum "," "{" "}" (
             map (fn (f, e) =>
               Pretty.block [str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs
           )
       | ml_from_expr fxy (ILookup ([], v)) =
           str v

       | ml_from_expr _ e =
           error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
     and ml_mk_app f es =
       if is_cons f andalso length es > 1
       then
-        [(str o resolv) f, Pretty.gen_list " *" "(" ")" (map (ml_from_expr BR) es)]
+        [(str o resolv) f, Pretty.enum " *" "(" ")" (map (ml_from_expr BR) es)]
       else
         (str o resolv) f :: map (ml_from_expr BR) es
     and ml_from_app fxy =
       from_app ml_mk_app ml_from_expr const_syntax fxy;
     fun ml_from_funs (ds as d::ds_tl) =

       let
         fun from_sctxt [] = str ""
           | from_sctxt vs =
               vs
               |> map (fn (v, cls) => str ((upper_first o resolv) cls ^ " " ^ lower_first v))
-              |> Pretty.gen_list "," "(" ")"
+              |> Pretty.enum "," "(" ")"
               |> (fn p => Pretty.block [p, str " => "])
       in 
         vs
         |> map (fn (v, sort) => map (pair v) sort)
         |> Library.flat