diff -r 81ba62493610 -r f1ed1e9cd080 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Tue Feb 25 17:06:17 2014 +0000
+++ b/src/HOL/Library/Code_Target_Int.thy	Tue Feb 25 19:07:14 2014 +0100
@@ -12,6 +12,10 @@
 
 declare [[code drop: integer_of_int]]
 
+context
+includes integer.lifting
+begin
+
 lemma [code]:
   "integer_of_int (int_of_integer k) = k"
   by transfer rule
@@ -86,6 +90,7 @@
 lemma [code]:
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
   by transfer rule
+end
 
 lemma (in ring_1) of_int_code_if:
   "of_int k = (if k = 0 then 0
@@ -105,7 +110,7 @@
 
 lemma [code]:
   "nat = nat_of_integer \<circ> of_int"
-  by transfer (simp add: fun_eq_iff)
+  including integer.lifting by transfer (simp add: fun_eq_iff)
 
 code_identifier
   code_module Code_Target_Int \<rightharpoonup>