[isabelle-dev] Probable bug in let_simp simproc

[Thomas Sewell]

I spent a bit of yesterday trying to discover why the standard simpset 
was taking forever to simplify a large term I happen to have.

The term is folded down in such a manner that unfolding Let_def will 
cause it to grow extremely large, which turns out to be what is 
happening. Deleting the let_simp simproc from the simpset solves the 
problem.

The let_simp simproc is written in two halves. The first bit I can 
easily understand, and if I produce a simproc with just that code it 
does what is expected.

The second half is commented "Norbert Schirmer's case", and is 
incomprehensible to me at the moment. Does anyone know, broadly, what it 
is meant to do? If I knew that I might be able to figure out what the 
problem was.

Yours,
     Thomas.