--- a/src/ZF/Cardinal.ML Thu Jun 06 16:20:27 1996 +0200
+++ b/src/ZF/Cardinal.ML Fri Jun 07 10:56:37 1996 +0200
@@ -744,8 +744,7 @@
by (etac nat_induct 1);
by (fast_tac (ZF_cs addIs [wf_onI]) 1);
by (rtac wf_onI 1);
-by (asm_full_simp_tac
- (ZF_ss addsimps [wf_on_def, wf_def, converse_iff, Memrel_iff]) 1);
+by (asm_full_simp_tac (ZF_ss 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 (ZF_cs addSEs [mem_irrefl] addEs [mem_asym]) 2);