Remove eqtype declaration for term type

Added size functions for finite sets, maps, and bags.

These are helpful for measures supporting recursive definitions and
induction schemes. The size functions have been added to the TypeBase,
with the intent that Induct, Induct_on, Cases, and Cases_on should be
applicable. (However, this has not been checked yet, so these might
not work.)

The size of a finite set is the number of elements in it, plus the
sizes of all the elements. (The size of a set with 0 as an element is
larger than that set with the zero deleted.)

The size of a finite map is the number of mapped elements, plus the
sizes of the mapped elements. Key size is ignored.

The size of a finite multiset is the number of elements in the
multiset plus the sizes of the elements. There are more extensive
orderings (e.g. the multiset order) but they aren't measures, which is
important for the way termination proofs are automated.

Removed Lib.gather. Use {Lib,List}.filter instead.

Wide-ranging change to make the TypeBase export an interface forcing users
to be concerned about which theory their types are from. Interactive users
of the "induction_of", "axiom_of" and similar functions are thrown the only
bone: they can effectively omit the theory parameter by using "" instead
of a theory name.
Prompted by a bug found by Tom Ridge where it was impossible to define
a pattern matching function on a type with the same name as another type
because the pattern-matching code was using dest_type and TypeBase.read
on just the type-operator name.

A load of changes aimed at supporting records better. And some other
odds and ends.

Preliminary addition of support for ML execution.