--- a/src/ZF/Cardinal.ML Fri Apr 04 11:32:44 1997 +0200
+++ b/src/ZF/Cardinal.ML Fri Apr 04 11:33:51 1997 +0200
@@ -748,7 +748,7 @@
by (asm_full_simp_tac (!simpset addsimps [wf_on_def, wf_def, Memrel_iff]) 1);
by (excluded_middle_tac "x:Z" 1);
by (dres_inst_tac [("x", "x")] bspec 2 THEN assume_tac 2);
-by (fast_tac (!claset addSEs [mem_irrefl] addEs [mem_asym]) 2);
+by (blast_tac (!claset addEs [mem_irrefl, mem_asym]) 2);
by (dres_inst_tac [("x", "Z")] spec 1);
by (Blast.depth_tac (!claset) 4 1);
qed "nat_wf_on_converse_Memrel";