Get holfoot executables to build given change to quotation filter

Not clear to me if these holfoot executables are tested once built,
but they do now at least build.

holfoot: tweaks to building binaries

- turn printing on again after loading "holfoot.state"
- include path for loading state in header.sml

Revise holfoot executable generation to use polyc

This makes things simpler on the whole I think and lets us not have to
worry about shared libraries and their locations.

cleanup of quantifier heuristics library

- more sensible names for guesses
- quantHeuristicsLib renamed to quantHeuristicsLibBase
- quantHeuristicsLibArgs renamed to quantHeuristicsLibParameters
- new shorter signature defined in quantHeuristicsLib
- adaptation of usage of quantHeuristicsLib

Mayor refactoring of the Holfoot-Parser. The parser now uses the abstract syntax of HOL internally, which allows it to pass typing information between different parts of the input much more efficiently. As a result, most type-annotations could be removed from the input files. Moreover, it's now possible to write HOL terms as expressions inside a program now. These expressions have to return a value of type num and may take program variables as input. For example programs like "x = ``MAX y z``" can be written now, where "x", "y" and "z" are variables of the programming language. A similar extension has been added for conditions of loops and if-then-else statements. Finally, there is a predicate for separating mapping and predicate for queues now.

create subdirectories mosml and poly that contain ML-variant specific code