diff -r 424c7b1489df -r 64eda8afe2b4 List.ML
--- a/List.ML	Tue Feb 15 07:55:22 1994 +0100
+++ b/List.ML	Tue Feb 15 10:05:17 1994 +0100
@@ -395,7 +395,7 @@
  "P(list_case(xs,a,f)) = ((xs=[] --> P(a)) & \
 \                         (!y ys. xs=Cons(y,ys) --> P(f(y,ys))))";
 by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (list_ss addsimps [list_case_Nil,list_case_Cons])));
+by(ALLGOALS(asm_simp_tac list_ss));
 by(fast_tac HOL_cs 1);
 val expand_list_case = result();