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

[Stefan Berghofer]

Makarius wrote:
> It is not so easy to get an exception trace here.  Wrapping up
> Simplifier.generic_simp_tac as shown in the included changeset produces
> the following result:
> 
> Exception trace - TYPE ("Loose bound variable: B.7", [], [Bound 7])
> Sign.type_check(2)typ_of(2)
> [...]
> Splitter().mk_case_split_tac(1)inst_lift(7)

Hi all,

this bug has now been fixed in the development version of Isabelle (see c0c453ce70a7).
It has been present at least since 1995 (see e.g. 1d8fa2fc4b9c). The problem occurred
when the head of a term (called h in function mk_cntxt) on the path leading to an
abstraction that needs to be removed happened to be a bound variable. To avoid this
problem, inst_lift now fully instantiates the variable P (denoting the context in which
the abstraction occurs) in the "trlift" theorem and applies it using compose_tac rather
that rtac.

Greetings,
Stefan