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 desymbolize: 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 desymbolize upper "" = if upper then "X" else "x"
-  | desymbolize upper s =
+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;
         val ys =
           if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
           else "x" :: xs;

           else
             (case Symbol.decode x of
               Symbol.Sym name => "_" :: raw_explode name @ sep xs
             | _ => sep xs);
         fun upper_lower cs =
-          if upper then nth_map 0 Symbol.to_ascii_upper cs
-          else
-            (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
-              Symbol.to_ascii_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;
       in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
 
 end;