fixed

--- a/src/HOL/ex/ThreeDivides.thy	Mon Feb 20 16:23:38 2006 +0100
+++ b/src/HOL/ex/ThreeDivides.thy	Mon Feb 20 21:51:50 2006 +0100
@@ -207,7 +207,7 @@
          (simp add: atLeast0LessThan)
     also have
       "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
-      by (simp add: setsum_rmv_upt cdef)
+      by (simp add: setsum_head_upt cdef)
     also note `Suc nd = nlen m`
     finally
     show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .