[isabelle-dev] AFP: PAPP_Impossibility not terminating

[Makarius]

On 17/04/2023 23:38, Makarius wrote:
> 
> The first bad revision is:
> changeset:   77808:b43ee37926a9
> user:        wenzelm
> date:        Mon Apr 10 22:38:18 2023 +0200
> summary:     performance tuning: replace Ord_List by Set();
> 
> 
> This is a change of the thm hyps field to make applications like 
> PAPP_Impossibility actually faster, but I did not notice that this is such an 
> application, and that it becomes very slow.
> 
> Even worse, it is not sufficient to take b43ee37926a9 back, because other 
> changes on top appear to cause similar problems.

I have now managed to revert several changes to make PAPP_Impossibility works 
again --- nothing pushed yet.


	Makarius