Quoting Alexander Krauss <kra...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev