diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Hyperreal/Series.ML
--- a/src/HOL/Hyperreal/Series.ML	Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Hyperreal/Series.ML	Wed Dec 10 15:59:34 2003 +0100
@@ -431,7 +431,7 @@
              simpset() addsimps [sumr_geometric ,sums_def,
                                  real_diff_def, real_add_divide_distrib]));
 by (subgoal_tac "1 / (1 + -x) = 0/(x - 1) + - 1/(x - 1)" 1);
-by (asm_full_simp_tac (simpset() addsimps [real_divide_eq_cancel1,
+by (asm_full_simp_tac (simpset() addsimps [
                       real_divide_minus_eq RS sym, real_diff_def]) 2); 
 by (etac ssubst 1); 
 by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1);