diff -r cb3612cc41a3 -r fc075ae929e4 src/HOL/Algebra/poly/LongDiv.thy
--- a/src/HOL/Algebra/poly/LongDiv.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -18,12 +18,10 @@
   "!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) --> 
   setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"
   apply (induct_tac d)
-  apply (induct_tac m)
-  apply (simp)
-  apply (force)
-  apply (simp)
-  apply (subst ab_semigroup_add.add_commute[of m])
-  apply (simp)
+   apply (induct_tac m)
+    apply (simp)
+   apply (force)
+  apply (simp add: ab_semigroup_add.add_commute[of m]) 
   done
 
 end