src/Pure/name.ML

           | desep xs = xs;
         fun desymb x xs =
           if is_valid x then x :: xs
           else
             (case Symbol.decode x of
-              Symbol.Sym name => "_" :: explode name @ sep xs
+              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)