[isabelle-dev] sledgehammer no longer works

[Makarius]

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