changeset 57492 | 74bf65a1910a |
parent 56073 | 29e308b56d23 |
child 61076 | bdc1e2f0a86a |
--- a/src/HOL/ZF/HOLZF.thy Wed Jul 02 17:34:45 2014 +0200 +++ b/src/HOL/ZF/HOLZF.thy Wed Jun 11 14:24:23 2014 +1000 @@ -168,7 +168,7 @@ theorem Domain: "Elem x (Domain f) = (? y. Elem (Opair x y) f)" apply (auto simp add: Domain_def Replacement) - apply (rule_tac x="Snd x" in exI) + apply (rule_tac x="Snd xa" in exI) apply (simp add: FstSnd) apply (rule_tac x="Opair x y" in exI) apply (simp add: isOpair Fst)