capitalize even more carefully (see 5ac67041ccf8), e.g. relevant for option "z3_non_commercial" and prospective "MaSh";

--- a/src/Pure/General/word.scala	Sun May 25 17:08:46 2014 +0200
+++ b/src/Pure/General/word.scala	Mon May 26 13:29:16 2014 +0200
@@ -43,10 +43,9 @@
     }
 
   def perhaps_capitalize(str: String): String =
-    str match {
-      case Case(c) if c != Lowercase => str
-      case _ => capitalize(str)
-    }
+    if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
+      capitalize(str)
+    else str
 
   sealed abstract class Case
   case object Lowercase extends Case