[isabelle-dev] HOL-Proofs slow

[Makarius]

On Sun, 21 Oct 2012, Makarius wrote:

> 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.

It is indeed the above changeset, notably the two code_simp invocations 
here:

http://isabelle.in.tum.de/repos/isabelle/rev/744934b818c7#l9.7

Is there a way to bypass that in Main HOL?


 	Makarius