strip_binder will vary unbound variables

[ordinarymath]

Given a term like this ?q r. ?r q. (n' = q * m + r) /\ r < m Calling strip_exists on results in

`[“q'”, “r'”, “r”, “q”], “n' = q * m + r ∧ r < m”`

While repeatedly calling dest_exists via

fun strip_exists1 tm =
   let fun dest_exist_opt tm = SOME (dest_exists tm) handle HOL_ERR _ => NONE
       fun strip A tm =
           case dest_exist_opt tm of
               NONE => (List.rev A, tm)
             | SOME (x,tm') => strip (x::A) tm'
   in
      strip [] tm
   end

results in

[“q”, “r”, “r”, “q”], “n' = q * m + r ∧ r < m”)