diff -r 9eedaafc05c8 -r 74bf65a1910a src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jul 02 17:34:45 2014 +0200
+++ b/src/HOL/Divides.thy	Wed Jun 11 14:24:23 2014 +1000
@@ -461,7 +461,7 @@
 apply (case_tac "y = 0") apply simp
 apply (auto simp add: dvd_def)
 apply (subgoal_tac "-(y * k) = y * - k")
- apply (erule ssubst)
+ apply (simp only:)
  apply (erule div_mult_self1_is_id)
 apply simp
 done
@@ -470,8 +470,7 @@
 apply (case_tac "y = 0") apply simp
 apply (auto simp add: dvd_def)
 apply (subgoal_tac "y * k = -y * -k")
- apply (erule ssubst)
- apply (rule div_mult_self1_is_id)
+ apply (erule ssubst, rule div_mult_self1_is_id)
  apply simp
 apply simp
 done