strip quantifier variants can differ from repeatedly calling dest quantifier when encountering boundvars holding the same name

[ordinarymath]

Given a term of the form Abs(Fv("x",_),(Abs(Fv("x",_),_) Calling strip_abs on it differs from repeatedly calling dest_abs on it. See this example

val abs = mk_abs (``x':bool``,mk_abs (``x:bool``,``x /\ x'``))
val abs' = rename_bvar "x" abs
val test = strip_abs abs'
val check = (I ## dest_abs) (dest_abs abs')

which gives this result

val abs = “λx' x. x ∧ x'”: term
val abs' = “λx x'. x' ∧ x”: term
val test = ([“x'”, “x”], “x ∧ x'”): term list * term
val check = (“x”, (“x'”, “x' ∧ x”)): term * (term * term)