diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Real/Hyperreal/Series.ML
--- a/src/HOL/Real/Hyperreal/Series.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Series.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -94,9 +94,9 @@
     [real_minus_add_distrib]));
 qed "sumr_minus";
 
-context Arith.thy;
+context Arithmetic.thy;
 
-goal Arith.thy "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
+Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
 by (auto_tac (claset() addSDs [not_leE],simpset()));
 qed "lemma_not_Suc_add";