[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.

Regards,
  Peter


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
variables:
  x :: 'a
  ?foo, ?foo3 :: 'a \<Rightarrow> bool








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