--- a/src/HOL/Int.thy Fri Feb 15 08:31:30 2013 +0100
+++ b/src/HOL/Int.thy Fri Feb 15 08:31:31 2013 +0100
@@ -853,7 +853,7 @@
apply (rule nat_mono, simp_all)
done
-lemma nat_numeral [simp, code_abbrev]:
+lemma nat_numeral [simp]:
"nat (numeral k) = numeral k"
by (simp add: nat_eq_iff)