HomeIsabelle/Phabricator

allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c…