[isabelle-dev] HOL-Proofs slow

Makarius makarius at sketis.net
Sun Oct 21 23:32:55 CEST 2012

HOL-Proofs has become very slow, see

I first thought it would be related to 1167c1157a5b (haftmann on 
src/Pure/Proof/extraction.ML), which is not immediately easy to follow in 
every detail.

Bijection then produced this:

The first bad revision is:
changeset:   49948:744934b818c7
user:        haftmann
date:        Sat Oct 20 09:12:16 2012 +0200
summary:     moved quite generic material from theory Enum to more appropriate places

I can't say for sure if this is a correct result of the bijection, but it 
fits approximately in the time interval from my last successful (fast) 
test of everything.


More information about the isabelle-dev mailing list