HomeIsabelle/Phabricator

clarified modules: avoid multiple uses of the same ML file;