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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
