[isabelle] Unexpected flex-flex pair with FOCUS

Hi all,
consider the minimal example below. Why does FOCUS_PARAMS (and,
similarly, FOCUS and FOCUS_PREMS) produce a flex-flex pair here?
I would have expected this not to change the goal at all.


schematic_lemma "?foo x"
  apply (tactic {* Subgoal.FOCUS_PARAMS (K all_tac) @{context} 1*})

goal (1 subgoal):
 1. ?foo3 x
flex-flex pairs:
  ?foo3 x =?= ?foo x
  x :: 'a
  ?foo, ?foo3 :: 'a \<Rightarrow> bool

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