Revert "Eta-expand GEN_REWRITE_CONV so that bounded rewrites work better"

This reverts commit f83604e8d33cfea9322bc51e3716ec3d2b149ad0.

It turns out that this has serious efficiency effects.

Eta-expand GEN_REWRITE_CONV so that bounded rewrites work better

Things like

Once th

generate a reference when add_rewrites is called, so add_rewrites
should only be called when there is a term argument to be applied to
rather than in advance, which has the effect of sharing the
exhaustible reference between multiple arguments.

Thanks to Johannes Åman Pohjola for the bug report.

eliminated some ref-matches

Up to hol.state0

Remove TABs in some source code, replacing them with spaces

Use Emacs's conception of how many spaces the TAB was
representing (and the M-x untabify command).

This may not line up with the author's original conception, but then,
using TABs makes it impossible to tell just what the original
conception was in the first place anyway.

Should probably script this over all of repository (excluding
makefiles of course), and use standard expand or col utilities rather
than emacs.

More moving lcsymtacs implementations elsewhere

Eventually lcsymtacs will just be a bunch of 'open' declarations, and
then people won't bother to include it at all.

Fix a bug where REWRITE_TAC and friends with rewrite |- T could loop.

Change src/bool to src/1 as a prelude to experimentation!