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

also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg

reveal Skolems in new Metis

don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions

slacker version of "fastype_of", in case a function has dummy type

don't stumble on Skolem names

conceal old Skolems in new Metis

don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs

use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is

properly unmangle names in path finder

only uncombine combinators in textual Isar proofs, not in Metis

properly locate helpers whose constants have several entries in the helper table

skip "hBOOL" in new Metis path finder

don't pass "~ " to new Metis

tuning

gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings

temporarily document "metisX"

use "metisX" as fallback, since it's much faster than "metisFT"

temporarily added "MetisX" as reconstructor and minimizer

ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)

show what failed to play

refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow

tuning

killed odd connectives

added Metis examples to test the new type encodings

tuned CASC method

clean up unnecessary machinery -- helpers work also with monomorphic type encodings

added support for helpers in new Metis, so far only for polymorphic type encodings