rewrote the TPTP problem generation code more or less from scratch; there is now an explicit AST data structure which will make it easy to support alternative formats (e.g., DFG, sorted TPTP, sorted DFG); also, if "full_types" is enabled, "hAPP" is then tagged properly

rename functions

merged

unfold_fun_n

pervasive tuning of code

explicit printing function for applify

fail with low-level exception, not user error;

eliminated some unused bindings;

recovered some indentation from the depths of time;

cleaned by using descending instead of lifting

merged

move function

compile

compile

more elegant cheating

Sledgehammer can save some msecs by cheating

more precise error message for remote ATPs

move blacklisting completely out of the clausifier; the only reason it was in the clausifier as well was the Skolem cache

rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems

move "nice names" from Metis to TPTP format

move functions not needed by Metis out of "Metis_Clauses"

no setup is necessary anymore

adapt call

remove obsolete component of CNF clause tuple (and reorder it)

killed "expand_defs_tac"; it has no raison d'etre now that Skolemization is always done "inline"; the comment in the code suggested that it was used for other things as well but the code clearly did nothing if no Skolem "Frees" were in the problem

get rid of Skolem cache by performing CNF-conversion after fact selection

always perform "inline" skolemization, polymorphism or not, Skolem cache or not

always perform relevance filtering on original formulas