generate less type information in polymorphic case

Metis code cleanup

enable new Metis

made "explicit_apply"'s smart mode (more) complete

fall back in case path finder fails -- these errors are sometimes salvageable

compile

change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A"

marked "metisF" as legacy -- nobody uses it or needs it

more preparations towards hijacking Metis

remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"

don't mention "metisX" so much in the docs -- it will go away soon

reintroduced metisFT in example

make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s

imported patch metis_reconstr_give_type_infer_a_chance

make "metisX"'s default more like old "metis"

whitespace tuning

tuned Metis examples

more through tests of new Metis

improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)

fixed type helper indices in new Metis

improved ATP clausifier so it can deal with "x => (y <=> z)"

avoid renumbering hypotheses

fixed reconstruction of new Skolem constants in new Metis

don't translate new Skolemizer assumptions in new Metis

tuning

fixed detection of Skolem constants in type construction detection code

make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)

tuning