more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts;
tuned whitespace;