Generalise congruence API to handle terms with free vars as equivs.

Allow congruence rules for relations other than equality to be added
via the congs field of a ss-fragment. This means that using the
special 'Cong' marker also works.

Keep list of relations sorted and remove duplicates. Before this
change, simpsets would get increasing numbers of copies of the base
equality relation.

Change relations that have congruence rules stored for them
(they have to be preorders) to be stored as terms rather than string
pairs (the latter encoded theory and term name, allowing constants
only). The samerel function is now what should be used to determine
if two preorders are compatible. The use of same_const and aconv
means that only single constants can be used polymorphically, but
arbitrary monomorphic terms can be used elsewhere. (It's possible
this breaks Thomas Türk's examples; I have run selftest 1 on
everything else.)

Changed mk_travrules to use the new interface of CONGPROC

Fixed a small bug in mk_preorder

Paired syntax.

Fixes in order to remove library file dependencies on global grammars.

Initial revision