HomeIsabelle/Phabricator

avoid legacy binding errors in Sledgehammer Isar proofs