theory Barf
imports Main
begin

  lemma
  shows nothing
  proof -
    let ?x0 = 100
    let ?x1 = 101
    let ?y = "\<lambda>i. if i = 0 then ?x0 else ?x1"
    have "?y 0 = ?x0" by presburger
    let ?x = 102
    have "?y 0 = ?x0" oops (* ?x0 is now 102 *)

end