[isabelle-dev] Metis: Unused Theorem Reduces Run-Time?

[Tjark Weber]

On Fri, 2013-01-18 at 19:29 +0100, Jasmin Christian Blanchette wrote:
> What's your concrete suggestion here?

It's more of a curiosity than an issue, of course. Otherwise, I would
suggest to: First, make sure that the behavior is not due to a bug or
silly inefficiency in the metis code. Second, offer a way to suppress
the warning.

Best regards,
Tjark