src/Tools/Code/code_ml.ML

     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
           ((str o deresolve_inst) inst ::
             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
       | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
-          [str (if k = 1 then first_upper v ^ "_"
-            else first_upper v ^ string_of_int (i+1) ^ "_")]
+          [str (if k = 1 then Name.enforce_case true v ^ "_"
+            else Name.enforce_case true v ^ string_of_int (i+1) ^ "_")]
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
       (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
           print_app is_pseudo_fun some_thm vars fxy (const, [])

     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
           brackify BR ((str o deresolve_inst) inst ::
             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
       | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
-          str (if k = 1 then "_" ^ first_upper v
-            else "_" ^ first_upper v ^ string_of_int (i+1))
+          str (if k = 1 then "_" ^ Name.enforce_case true v
+            else "_" ^ Name.enforce_case true v ^ string_of_int (i+1))
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
       (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
           print_app is_pseudo_fun some_thm vars fxy (const, [])

             fun print_classparam_decl (classparam, ty) =
               print_val_decl print_typscheme
                 (Constant classparam, ([(v, [class])], ty));
             fun print_classparam_field (classparam, ty) =
               print_field (deresolve_const classparam) (print_typ NOBR ty);
-            val w = "_" ^ first_upper v;
+            val w = "_" ^ Name.enforce_case true v;
             fun print_classparam_proj (classparam, _) =
               (concat o map str) ["let", deresolve_const classparam, w, "=",
                 w ^ "." ^ deresolve_const classparam ^ ";;"];
             val type_decl_p = concat [
                 str "type",

 fun ml_program_of_program ctxt module_name reserved identifiers =
   let
     fun namify_const upper base (nsp_const, nsp_type) =
       let
         val (base', nsp_const') =
-          Name.variant (if upper then first_upper base else base) nsp_const
+          Name.variant (if upper then Name.enforce_case true base else base) nsp_const
       in (base', (nsp_const', nsp_type)) end;
     fun namify_type base (nsp_const, nsp_type) =
       let
         val (base', nsp_type') = Name.variant base nsp_type
       in (base', (nsp_const, nsp_type')) end;