
diff -r aa83d943c18b -r f2a32197a33a src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Thu Nov 08 19:55:37 2012 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Thu Nov 08 20:02:41 2012 +0100
@@ -244,7 +244,7 @@
  apply (elim dividesE, intro dividesI, assumption)
  apply (rule l_cancel[of c])
     apply (simp add: m_assoc carr)+
-apply (fast intro: divides_mult_lI carr)
+apply (fast intro: carr)
 done
 
 lemma (in comm_monoid) divides_mult_rI [intro]:




