Belatedly replying to say I've read the open access paper now. And as I did I was really wondering how that fuzzy unification matching based on predicate names could work to produce reliable results for the purposes sought. Though to be fair it's 30+ years since I studied theorem proving and Prolog with Roy Dyckhoff! However I am a bit encouraged by your comments above. I maybe wasn't completely losing the plot. I'd be interested to see any future writeup re the version using Isabelle. Thanks for the interesting read!