HomeIsabelle/Phabricator

slightly more explicit error, without going into the graph of proof futures;