src/ZF/AC/AC17_AC1.thy

--- a/src/ZF/AC/AC17_AC1.thy	Wed Jul 10 16:07:52 2002 +0200
+++ b/src/ZF/AC/AC17_AC1.thy	Wed Jul 10 16:54:07 2002 +0200
@@ -235,7 +235,7 @@
 lemma AC3_AC1_lemma:
      "b\<notin>A ==> (\<Pi>x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi>x \<in> A. x)"
 apply (simp add: id_def cong add: Pi_cong)
-apply (rule_tac b = "A" in subst_context, fast)
+apply (rule_tac b = A in subst_context, fast)
 done
 
 lemma AC3_AC1: "AC3 ==> AC1"