[isabelle] Problem "exception TYPE raised: Loose bound variable"



Dear all,

recently I stumbled upon an "Loose bound variable" exception in "sign.ML".

The problem occurred when I wanted to show that a certain operation is
invariant under record-updates.

If I do the proof incrementally (first proving invariance for all the auxiliary 
functions), then everything works fine. However, doing the same kind of reasoning
directly without explicitly considering the auxiliary functions, then calling the
simplifier led to the above exception.

The problem occurs in both Isabelle2013-RC2 and in the development version
(80660c529d74)

I just want to report this problem, a small theory file is attached.
I tried to simplify the example as much as possible, but several further 
simplification which I tried resulted in normal behavior without the exception.

Kind regards,
René

Attachment: Test.thy
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.