[isabelle] Simplifier fails when dealing with mix of Pure and HOL terms

[Makarius]

On 28/11/2025 16:47, Lawrence Paulson via isabelle-dev wrote:
> I tested a patch a little bit. If we catch the exception, the simplifier still fails (as one would expect). The warning "cannot atomize goal" no longer appears. For some reason, “apply simp?” still fails.

Please, no adhoc patches or "big fixes", which are usually wrong. I've spent 
so many decades sorting out problems introduced by presumed "fixes".


Step 0 is to use induction over the history of the sources (using "hg 
bisect"). It reveals this notable point:

The first bad revision is:
changeset:   71989:bad75618fb82
user:        haftmann
date:        Thu Jul 02 12:10:58 2020 +0000
summary:     extraction of equations x = t from premises beneath meta-all

This change is not immediately obvious, it belongs to a greater context.

Step 1 is to show this to the author, Florian Haftmann, in order to amend, 
finish, improve on it.


(It is certainly not relevant for the Isabelle2025-1 release, as a 
non-regression from previous releases.)


	Makarius