Get some extra timings with these tests.

A useful extra for Lib. (Also a slight fix for big.term.tests to stop it
printing out huge terms.)

Support for making term destructors use "same_const". Also some effort
at making bulk term operations more predictable.

Introduction of strip_binder into kernel. This allows many consecutive
binders to be stripped off efficiently. It takes about 18 seconds to
build an abstraction with a million binders, and about 26 seconds to
take it back apart.

Users may notice that the prettyprinter is lying to them. This is
because the prettyprinter currently iterates "dest_abs" to break terms
down, which can give different renaming behaviour that the bulk
processing of strip_{abs,forall,exists}. It was too hard to fully
simulate the processing of iterated dest_abs.

Big terms can be constructed in finite time now. On my laptop,

list_mk_abs(1Mvars,list_mk_conj 1Mvars)

gets built in about 20 seconds. list_mk_forall and list_mk_exists are
twice as slow. If you are going to build terms with lots of
binding, please use these things in favour of

itlist (curry mk_forall) vlist tm

which 1) is slow because of the iterated mk_forall and 2) blows the stack
because of the itlist, at least in MoscowML, which allocates the call stack
on the stack.

Still to do: 1) upgrading this treatment to strip_abs, strip_forall, and
strip_exists; 2) upgrading it to paired abstractions; 3) efficienct versions
of SPECL and GENL (if possible); and 4) a rewriter that uses these facilities
to traverse deeply nested binders efficiently (this will (1) be a first
order rewriter and ... uh lost my train of thought).

There are some tests in src/0/big.term.tests. These should also be fleshed
out to have more strenuous tests, say ones with multiple parallel deeply
nested scopes.

... uh, the above 20 second claim is true if the list_mk_conj had
been done previously (I was mainly testing list_mk_abs).

The implementation uses Polyhash to represent the list of variables to
be bound, and utilizes continuation passing style to get tail recursion.
Otherwise, I couldn't get to 500K variables without blowing the stack.