more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML);