--- a/src/ZF/Finite.ML Thu Sep 05 18:29:43 1996 +0200
+++ b/src/ZF/Finite.ML Thu Sep 05 18:30:13 1996 +0200
@@ -57,7 +57,7 @@
goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
by (etac Fin_induct 1);
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
-by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
+by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_simps) 1);
by (safe_tac ZF_cs);
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
by (asm_simp_tac Fin_ss 1);
@@ -128,7 +128,7 @@
goal Finite.thy "!!b A. b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
by (etac FiniteFun.induct 1);
by (simp_tac (ZF_ss addsimps subset_empty_iff::FiniteFun.intrs) 1);
-by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
+by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_simps) 1);
by (safe_tac ZF_cs);
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
by (dtac (spec RS mp) 1 THEN assume_tac 1);