
diff -r 23917e861eaa -r a41435469559 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:33 2017 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:35 2017 +0200
@@ -59,7 +59,7 @@
 
 lemma [code abstract]:
   "integer_of_nat (nat_of_num n) = integer_of_num n"
-  by transfer (simp add: nat_of_num_numeral)
+  by (simp add: nat_of_num_numeral integer_of_nat_numeral)
 
 lemma [code abstract]:
   "integer_of_nat 0 = 0"




