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

[Lawrence Paulson]

I think the exception is coming from a low-level function called yield_singleton, which is called by the version of prove_conv in Provers/quantifier1.ML. Several of the simprocs there contain the snippet

	SOME (prove_conv ctxt …) 

and each of these could raise exception List.Empty, which would not be caught and would blow up at the top level.

So if it is not too late, I propose adding an exception handler to each 

	handle List.Empty => NONE.

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.
>