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

[Makarius]

On 28/11/2025 15:22, Lawrence Paulson via isabelle-dev wrote:
> I made a little search. There are 115 occurrences of "simproc del: defined_all" in the distribution and AFP. I'm not sure what this thing does but perhaps it needs urgent attention.

It has been there for 5 years already, so nothing is urgent here in terms of 
the Isabelle2025-1 release.

A proper stable release requires some discipline.


	Makarius