--- a/src/Pure/name.ML Mon Oct 08 15:42:43 2018 +0200
+++ b/src/Pure/name.ML Mon Oct 08 17:12:28 2018 +0200
@@ -151,9 +151,9 @@
(* names conforming to typical requirements of identifiers in the world outside *)
-fun enforce_case' false cs =
+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 =
+ | enforce_case' true cs =
nth_map 0 Symbol.to_ascii_upper cs;
fun enforce_case upper = implode o enforce_case' upper o raw_explode;