diff -r ee90c67502c9 -r 18fbca265e2e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Sep 16 15:30:17 2013 +0200
+++ b/src/HOL/Int.thy	Mon Sep 16 15:30:20 2013 +0200
@@ -1660,12 +1660,7 @@
 
 text {* De-register @{text "int"} as a quotient type: *}
 
-lemmas [transfer_rule del] =
-  int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
-  plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
-  int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
-  nat.transfer int.right_unique int.right_total int.bi_total
-
-declare Quotient_int [quot_del]
+lifting_update int.lifting
+lifting_forget int.lifting
 
 end