diff -r b66639331db5 -r baef1c110f12 src/Pure/name.ML
--- a/src/Pure/name.ML	Thu May 01 09:30:35 2014 +0200
+++ b/src/Pure/name.ML	Thu May 01 09:30:36 2014 +0200
@@ -31,6 +31,7 @@
   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;
 
@@ -150,6 +151,13 @@
 
 (* 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 =
@@ -171,13 +179,7 @@
             (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;