diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/Tools/spell_checker.scala --- a/src/Pure/Tools/spell_checker.scala Thu Jun 01 21:24:33 2017 +0200 +++ b/src/Pure/Tools/spell_checker.scala Thu Jun 01 21:43:36 2017 +0200 @@ -57,7 +57,7 @@ class Dictionary private[Spell_Checker](val path: Path) { - val lang = path.split_ext._1.base.implode + val lang = path.split_ext._1.base_name val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang) override def toString: String = lang }