diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Univ.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -147,7 +147,7 @@
 
 lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
 apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst])
-apply (rule_tac x1 = "i" in Vfrom_rank_eq [THEN subst])
+apply (rule_tac x1 = i in Vfrom_rank_eq [THEN subst])
 apply (subst rank_succ)
 apply (rule Ord_rank [THEN Vfrom_succ_lemma])
 done