fixed proof to cope with the default of equalityCE instead of equalityE

--- a/src/HOL/List.ML	Thu Jun 29 12:14:45 2000 +0200
+++ b/src/HOL/List.ML	Thu Jun 29 12:15:08 2000 +0200
@@ -477,6 +477,8 @@
 
 Goal "set[i..j(] = {k. i <= k & k < j}";
 by (induct_tac "j" 1);
+by (ALLGOALS Asm_simp_tac);
+by (etac ssubst 1);
 by Auto_tac;
 by (arith_tac 1);
 qed "set_upt";