src/HOL/Old_Number_Theory/Pocklington.thy

--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -161,7 +161,7 @@
     and q12': "y + n*q1' = y'+n*q2'" unfolding nat_mod by blast+
   from th[OF q12 q12' yx yx']
   have "(x - y) + n*(q1 + q2') = (x' - y') + n*(q2 + q1')"
-    by (simp add: right_distrib)
+    by (simp add: distrib_left)
   thus ?thesis unfolding nat_mod by blast
 qed