[isabelle-dev] Odd failure to match local statement with pending goal.

[Stefan Berghofer]

Quoting Alexander Krauss <krauss at in.tum.de>:
> The same can be done in low-level ML, using just "rtac", which  
> suggests that the error is somewhere in the underlying  
> Thm.biresolution etc. So far, I have not looked any further...

Hi Alex and Larry,

I guess the culprit is function rename_bvs in Pure/thm.ML, which is used
by bicompose_aux. The rationale behind this function is to make rule
applications preserve as many of the variable names in the goal as possible,
to make it more readable for the user. According to the comment before this
function, it renames "all bound variables and some unknowns", and I think the
"some unknowns" part is causing the problem. In your example the conclusion
of rule R with bound variables s and t is matched against a goal where
both bound variables are named c, which causes rename_bvs to rename both
schematic variables ?s and ?t in R to ?c. The function already contains
a rudimentary check for name clashes, but this has to be extended.
Thanks again for narrowing down the problem!

Greetings,
Stefan