[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

[Makarius]

On Fri, 19 Oct 2012, Lukas Bulwahn wrote:

>> Operations like Simplifier.context, Simplifier.inherit_context should 
>> help here.  Once that is repaired, I will see if the warning can now be 
>> made an error that is more explicit about the reasons.
>> 
> I am certainly in favour of this. First, tool developers mainly react on 
> errors with test runs, but do not see the warnings. Secondly, users do 
> not know who to report those warnings and do not know if they are caused 
> by their scripts or the tools.

Historically, the weak warning was a necessity due to too many simprocs 
still not working with the context.

Let's hope that it can be easily switched to an explicit error after so 
many years now.


 	Makarius