[isabelle-dev] Interrupt exception

[Makarius]

On Wed, 15 Jul 2009, Lucas Dixon wrote:

>>>   apply (unfold Product_Type.pair_collapse[symmetric, of "al"])
>> 
>> The equation Product_Type.pair_collapse[symmetric, of "al"] can be
>> unfolded forever, so the method invocation does not terminate, leading
>> to an unspecified behaviour of the system!
>
> The point was just that unfold should probably be giving an error message of 
> some more readable sort.

The interrupt exception is probably produced by the Poly/ML runtime system 
when it runs out of resources.  The behaviour might have changed a bit in 
recent internal versions.  Which one did you use?


 	Makarius