clarified Symbol.scan_ascii_id; ATP: follow change from Symbol.scan_id to Symbol.scan_ascii_id, assuming that this was meant here, not fully symbolic Isabelle identifiers;