Lift Table functor out of fromIsabelle into src/portableML

This code is Isabelle's workhorse version of our Binarymap. It has a
better API for working with maps into lists of values, and is also
better in that its use of a functor means that the types of
maps/dictionaries/tables using different comparison functions are
different.

I have altered it to use HOL style comparison functions that are
curried rather than tupled. (I.e., in Isabelle the equivalents of our
various op_<operation> functions are take a comparison function that
takes a pair of arguments; our tradition is to use a curried
function.)

I have also added pretty-printing, requiring KEY-structures to provide
a pp function. (These functions ignore depth arguments for the
moment.)

Finally, there are a number of knock-on effects in the fromIsabelle
directory.