[isabelle-dev] HOL-Proofs slow

[Makarius]

On Mon, 22 Oct 2012, Florian Haftmann wrote:

>> 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.
>
> It indeed isn't, but the effect is idempotent.
>
> To my defence, reordering arguments is not very comprehensible from a diff.

In such cases, the general question is if making the sources "canonical" 
has any purpose.  It is rather old material by Stefan Berghofer, written 
in the typical style from around 2000, and not going to be revisited in 
the foreseeable future.  There are no fundamental known problems with it. 
So why change it in the first place?

Concerning the digestability of the changeset, it did not turn out as bad 
as first anticipated.  Bitbucket has pretty good word-wise diffs.  So 
after spending about 45min with: 
https://bitbucket.org/makarius/isabelle/changeset/1167c1157a5b83b05bd259adb7ee9b7729d98303 
I came to the conclusion that the changeset is clean.


 	Makarius