Fix failing proofs after update to Metis 2.4

Update Metis to 2.4

updated to polyml-5.8.1-20200708: recent repository version for testing;

more robust protocol for "Timing ..." messages, notably for pide_session=true;

removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible…

Convert single bindings from mutual recursion into simple bindings.

The "setter" for a container refers to the container itself so any bindings…

Fix function name: they're mutual bindings not mutable.

When analysing the usage pattern of a recursive function we need to consider…

Fix use of "print" rather than "stream" for debugging.

separation of traditional bit operations

separation of traditional bit operations

no pide_session on macos: avoid odd "hang" of remote_build_history;

support generated preferences, i.e. non-strict system options;

factored out auxiliary theory

prefer explicit proof

factored out auxiliary theory

more operations for maps

tuned whitespace;

clarified signature;

use less memory on old hardware;

clarified log message (more uniform);

misc lemma tuning

explicit proofs for bit projections

misc lemma tuning

activated simproc defined_all

extraction of equations x = t from premises beneath meta-all

updated documentation

obsolete duplicates

removed superfluous dependency

a small aggiornamento for Z2

factored out ancient numeral representation

moved to Word_Lib

tuned whitespace

factored out ancient numeral representation

moved to Word_Lib

more explicit proofs

clarified options --- potentially more robust;

tuned message;