src/ZF/AC/AC16_lemmas.thy

--- a/src/ZF/AC/AC16_lemmas.thy	Wed Jul 10 16:07:52 2002 +0200
+++ b/src/ZF/AC/AC16_lemmas.thy	Wed Jul 10 16:54:07 2002 +0200
@@ -82,7 +82,7 @@
 apply (rule subsetI)
 apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast )
 apply (simp, erule bexE) 
-apply (rule_tac i=xa and j=x in Ord_linear_le)
+apply (rule_tac i=y and j=x in Ord_linear_le)
 apply (blast dest: le_imp_subset elim: leE ltE)+
 done