diff -r f329e59cebab -r 6ab5b4595f64 src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Mon Sep 01 19:17:37 2008 +0200
+++ b/src/HOL/ex/ThreeDivides.thy	Mon Sep 01 19:17:47 2008 +0200
@@ -210,7 +210,7 @@
          (simp add: atLeast0LessThan)
     also have
       "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
-      by (simp add: setsum_head_upt cdef)
+      by (simp add: atLeast0LessThan[symmetric] setsum_head_upt_Suc cdef)
     also note `Suc nd = nlen m`
     finally
     show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .