src/Pure/name.ML

   val invent: context -> string -> int -> string list
   val invent_names: context -> string -> 'a list -> (string * 'a) list
   val invent_list: string list -> string -> int -> string list
   val variant: string -> context -> string * context
   val variant_list: string list -> string list -> string list
+  val enforce_case: bool -> string -> string
   val desymbolize: bool option -> string -> string
 end;
 
 structure Name: NAME =
 struct

 fun variant_list used names = #1 (make_context used |> fold_map variant names);
 
 
 (* names conforming to typical requirements of identifiers in the world outside *)
 
+fun enforce_case' false cs = 
+      (if forall Symbol.is_ascii_upper cs then map else nth_map 0) Symbol.to_ascii_lower cs
+  | enforce_case' true cs = 
+      nth_map 0 Symbol.to_ascii_upper cs;
+
+fun enforce_case upper = implode o enforce_case' upper o raw_explode;
+
 fun desymbolize perhaps_upper "" =
       if the_default false perhaps_upper then "X" else "x"
   | desymbolize perhaps_upper s =
       let
         val xs as (x :: _) = Symbol.explode s;

           if is_valid x then x :: xs
           else
             (case Symbol.decode x of
               Symbol.Sym name => "_" :: raw_explode name @ sep xs
             | _ => sep xs);
-        fun upper_lower cs =
-          case perhaps_upper of
-            NONE => cs
-          | SOME true => nth_map 0 Symbol.to_ascii_upper cs
-          | SOME false =>
-              (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
-                Symbol.to_ascii_lower cs;
+        val upper_lower = Option.map enforce_case' perhaps_upper |> the_default I;
       in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
 
 end;