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

[Makarius]

On 28/11/2025 21:51, Makarius wrote:
> 
> 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

See also this NEWS entry from Isabelle2021:


* Simproc "defined_all" and rewrite rule "subst_all" perform more
aggressive substitution with variables from assumptions.
INCOMPATIBILITY, consider repairing proofs locally like this:

   supply subst_all [simp del] [[simproc del: defined_all]]


Which means that in these terms, the example by Hanno is "broken".

It is up to discussion, together with Florian, if this is good or bad. But we 
can definitely close the case as something urgent to be "fixed".


	Makarius