diff -r 9eedaafc05c8 -r 74bf65a1910a src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed Jul 02 17:34:45 2014 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Jun 11 14:24:23 2014 +1000
@@ -1655,6 +1655,7 @@
 using assms
 unfolding factors_def
 apply (safe, force)
+apply hypsubst_thin
 apply (induct fa)
  apply simp
 apply (simp add: m_assoc)