[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

[Dmitriy Traytel]

Hi all,

the following produces a "Loose bound variable" with Isabelle/4a15873c4ec9

theory Scratch
imports Main
begin

lemma "finite {y |y. ∃x. y ∈ f x}"
apply simp
oops

end

Fortunately, jedit treats a proof that used to work (but fails now due 
to the above) as a sorry, such that I can continue working on whatever 
follows in the theory until this issue is fixed.

Best wishes,
Dmitriy