add a penalty for lambda-abstractions;
the penalty will kick in only when the goal contains no lambdas, in which case Sledgehammer previously totally disallowed any higher-order construct; this was too drastic;
lambdas are dangerous because they rapidly lead to unsound proofs; e.g. COMBI_def COMBS_def not_Cons_self2 with explicit_apply

renaming

fiddle with relevance filter

update docs

reorganize options regarding to the relevance threshold and decay

make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
"max_relevant" is more reliable than "max_relevant_per_iter";
also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before;
SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)

simplify more code

cosmetics

get rid of "defs_relevant" feature;
nobody uses it and it works poorly

make SML/NJ happy