diff -r fe118a977a6d -r 773657d466cb src/ZF/List.ML
--- a/src/ZF/List.ML	Tue May 14 12:33:42 2002 +0200
+++ b/src/ZF/List.ML	Wed May 15 10:42:32 2002 +0200
@@ -238,7 +238,6 @@
 \          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
 by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
 qed_spec_mp "drop_length_Cons";
 
 Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";