# HG changeset patch
# User lcp
# Date 783859541 -3600
# Node ID 8fe0fbd768870a7b4ee7f7cf645e35fcc0fb7ff6
# Parent  c36f49c76d2230cd279faad29121d589dad0c833
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE

diff -r c36f49c76d22 -r 8fe0fbd76887 src/ZF/Cardinal_AC.ML
--- a/src/ZF/Cardinal_AC.ML	Thu Nov 03 08:34:53 1994 +0100
+++ b/src/ZF/Cardinal_AC.ML	Thu Nov 03 11:45:41 1994 +0100
@@ -77,7 +77,7 @@
 by (resolve_tac [exI] 1);
 by (rtac f_imp_injective 1);
 by (resolve_tac [Pi_type] 1 THEN assume_tac 1);
-by (fast_tac (ZF_cs addDs [apply_type] addEs [memberPiE]) 1);
+by (fast_tac (ZF_cs addDs [apply_type] addDs [Pi_memberD]) 1);
 by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1);
 val surj_implies_inj = result();