1.1 --- a/src/HOL/List.ML	Thu Jun 01 11:22:27 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Jun 01 13:28:00 2000 +0200
     1.3 @@ -1200,12 +1200,9 @@
     1.4  
     1.5  Goal "i+k < j --> [i..j(] ! k = i+k";
     1.6  by (induct_tac "j" 1);
     1.7 - by (Simp_tac 1);
     1.8 -by (asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
     1.9 -by (Clarify_tac 1);
    1.10 -by (subgoal_tac "n=i+k" 1);
    1.11 - by (Asm_simp_tac 2);
    1.12 -by (Asm_simp_tac 1);
    1.13 + by (asm_simp_tac (simpset() addsimps [less_Suc_eq, nth_append] 
    1.14 +                             addsplits [nat_diff_split]) 2);
    1.15 +by (Simp_tac 1);
    1.16  qed_spec_mp "nth_upt";
    1.17  Addsimps [nth_upt];
    1.18