diff -r 20ca66539bef -r 0f89104dd377 src/ZF/UNITY/ListPlus.ML
--- a/src/ZF/UNITY/ListPlus.ML	Wed Jul 10 16:07:52 2002 +0200
+++ b/src/ZF/UNITY/ListPlus.ML	Wed Jul 10 16:54:07 2002 +0200
@@ -335,16 +335,13 @@
 
 (** More on lists **)
 
-Goal
-"n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \
-\ --> nth(i, drop(n, xs)) = nth(n #+ i, xs)";
+Goal "n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \
+\               --> nth(i, drop(n, xs)) = nth(n #+ i, xs)";
 by (induct_tac "n" 1);
-by (ALLGOALS(Asm_full_simp_tac));
+by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
-by (case_tac "xb=Nil" 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
-by (Clarify_tac 1);
-by (auto_tac (claset() addSEs [ConsE], simpset()));
+by (etac list.elim 1);
+by Auto_tac;  
 qed_spec_mp "nth_drop";