Shortened a proof.

--- a/src/HOL/List.ML	Mon Jan 04 16:13:57 1999 +0100
+++ b/src/HOL/List.ML	Mon Jan 04 16:37:04 1999 +0100
@@ -856,8 +856,7 @@
 *)
 Goal "!n::nat. m <= n --> m <= foldl op+ n ns";
 by (induct_tac "ns" 1);
- by (Simp_tac 1);
-by (Asm_full_simp_tac 1);
+by Auto_tac;
 qed_spec_mp "start_le_sum";
 
 Goal "n : set ns ==> n <= foldl op+ 0 ns";