On Tue, 18 Mar 2008, Lawrence Paulson wrote:
> Attempting to use sledgehammer now generates dozens of "Legacy
> feature!" warnings. Also the output is no longer displayed. Does
> anybody know what is going on?
I am presently sorting out some longterm problems with facts storage.
Only some months ago, sledghammer was one more example, where the absence
of a proper thm table that works as anything else in the context (types,
consts) etc. prevented proper implementation of things like the skolem
cache.
Makarius
