
diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Divides.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -742,11 +742,11 @@
   apply (subst less_iff_Suc_add)
   apply (auto simp add: add_mult_distrib)
   done
-  from `n \<noteq> 0` assms have "fst qr = fst qr'"
+  from `n \<noteq> 0` assms have *: "fst qr = fst qr'"
     by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
-  moreover from this assms have "snd qr = snd qr'"
+  with assms have "snd qr = snd qr'"
     by (simp add: divmod_nat_rel_def)
-  ultimately show ?thesis by (cases qr, cases qr') simp
+  with * show ?thesis by (cases qr, cases qr') simp
 qed
 
 text {*




