# [isabelle] Smash flex-flex pairs in calculational reasoning

Dear list,
I have a sequence of calculational reasoning steps.
have "... f ... = ... (f some_argument)" for f
also have "some_other_subterm = ..."
finally have ... apply -

`In some of the steps I have abstracted over the concrete term by reasoning with some
``arbitrary f, which happens to be a function. Unfortunately, the "finally" step now
``introduces a flex-flex pair in "calculation", because f is applied to some_argument on the
``right-hand side of the first equation and some_other_subterm occurs in the ... part of the
``first right-hand side.
`

`The problem now is that the calculation at the end is completely unusable. Even a simple
``"apply -" raises an exception (in Isabelle2016):
`
exception THM 0 raised (line 820 of "thm.ML"):
forall_intr: variable "f" free in assumptions

`Why does also/finally not smash flex-flex pairs? Or is there some way to tell Isabelle to
``eliminate them?
`
Thanks in advance,
Andreas

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