# HG changeset patch
# User oheimb
# Date 829831380 -7200
# Node ID 7e84d8712a0bf63f4f82c3df92581dde0ec7b8bb
# Parent  a6b55b9d2f2219f06e5278f0627d79a6c03b898b
adapted proof of drop_succ_Cons: problem with non-confluent simpset removed

diff -r a6b55b9d2f22 -r 7e84d8712a0b src/ZF/List.ML
--- a/src/ZF/List.ML	Thu Apr 18 14:11:02 1996 +0200
+++ b/src/ZF/List.ML	Thu Apr 18 14:43:00 1996 +0200
@@ -109,7 +109,10 @@
 goalw List.thy [drop_def]
     "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
 by (etac nat_induct 1);
-by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons])));
+by (simp_tac (nat_ss addsimps [tl_Cons]) 1);
+by (rtac (rec_succ RS ssubst) 1);
+by (rtac (rec_succ RS ssubst) 1);
+by (asm_simp_tac ZF_ss 1);
 qed "drop_succ_Cons";
 
 goalw List.thy [drop_def]