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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
