src/HOL/Code_Numeral.thy

--- a/src/HOL/Code_Numeral.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -153,7 +153,7 @@
   "n < m \<longleftrightarrow> nat_of n < nat_of m"
 
 instance proof
-qed (auto simp add: code_numeral left_distrib intro: mult_commute)
+qed (auto simp add: code_numeral distrib_right intro: mult_commute)
 
 end