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

[Lawrence Paulson]

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.

Larry

> On 28 Nov 2025, at 11:00, Manuel Eberl <manuel at pruvisto.org> wrote:
> 
> This doesn't look like intended behaviour to me. I tracked the problem to the "defined_all" simproc, specifically to the ML function "Quantifier1.rearrange_all". If you remove that simproc from the simpset, the exception does not occur.
> 
> Perhaps this helps somebody who knows that part of the code understand what is going on.
>