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

[Lawrence Paulson]

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.

I investigated one theory where defined_all is suppressed (Auth/Guard/P1). From what I can tell, the reason was to keep the proof working as before and not that it was generating some sort of error.

Larry

> On 28 Nov 2025, at 15:36, Manuel Eberl <manuel at pruvisto.org> wrote:
> 
> The easiest and best way would probably be to simply declare goals that cannot be atomised as out of scope for the simproc and make it fail gracefully in such cases rather than have such a spectacular crash (as I think Larry suggested). On one hand, I for one don't see how this could introduce any problems (but I am aware that saying this is tempting fate). On the other hand, I don't think it is an urgent issue and can probably wait until after the release.