1.1 --- a/src/HOL/Algebra/poly/Degree.ML	Thu Nov 11 10:25:17 1999 +0100
     1.2 +++ b/src/HOL/Algebra/poly/Degree.ML	Thu Nov 11 10:25:29 1999 +0100
     1.3 @@ -285,7 +285,7 @@
     1.4  by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
     1.5  by (auto_tac
     1.6    (claset() addDs [not_leE],
     1.7 -   simpset() setloop (split_tac [expand_if])));
     1.8 +   simpset()));
     1.9  qed "bound_SUM_if";
    1.10  
    1.11  Goal
    1.12 @@ -297,8 +297,7 @@
    1.13  by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
    1.14  by (rtac SUM_cong 1);
    1.15  by (rtac refl 1);
    1.16 -by (asm_simp_tac 
    1.17 -  (simpset() setloop (split_tac [expand_if])) 1);
    1.18 +by (Asm_simp_tac 1);
    1.19  qed "up_repr";
    1.20  
    1.21  Goal