src/ZF/AC/AC16_lemmas.ML

--- a/src/ZF/AC/AC16_lemmas.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/ZF/AC/AC16_lemmas.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -137,7 +137,7 @@
 by (fast_tac (claset() addSEs [Diff_sing_eqpoll,
                 Diff_sing_eqpoll RS eqpoll_succ_imp_not_empty]) 1);
 by (resolve_tac [Union_eq_Un RSN (2, subst_elem)] 1 THEN (assume_tac 2));
-by (forward_tac [bspec] 1 THEN (assume_tac 1));
+by (ftac bspec 1 THEN (assume_tac 1));
 by (dresolve_tac [Diff_subset RS subsetD RSN (2, bspec)] 1 THEN (assume_tac 1));
 by (dtac Un_Ord_disj 1 THEN (assume_tac 1));
 by (etac DiffE 1);