HomeIsabelle/Phabricator

tuned --- avoid deprecated Predef.any2stringadd;