--- a/src/HOL/ex/Numeral.thy Sun Oct 16 14:48:00 2011 +0200
+++ b/src/HOL/ex/Numeral.thy Sun Oct 16 14:48:01 2011 +0200
@@ -893,7 +893,7 @@
lemma one_int_code [code]:
"1 = Pls One"
- by (simp add: of_num_One)
+ by simp
lemma plus_int_code [code]:
"k + 0 = (k::int)"