--- 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)