1.1 --- a/src/HOL/Int.thy	Tue Feb 19 13:37:07 2013 +0100
     1.2 +++ b/src/HOL/Int.thy	Tue Feb 19 15:03:36 2013 +0100
     1.3 @@ -1656,7 +1656,7 @@
     1.4    int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
     1.5    plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
     1.6    int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
     1.7 -  nat.transfer
     1.8 +  nat.transfer int.right_unique int.right_total int.bi_total
     1.9  
    1.10  declare Quotient_int [quot_del]
    1.11  

     2.1 --- a/src/HOL/Rat.thy	Tue Feb 19 13:37:07 2013 +0100
     2.2 +++ b/src/HOL/Rat.thy	Tue Feb 19 15:03:36 2013 +0100
     2.3 @@ -1129,7 +1129,7 @@
     2.4    rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer
     2.5    Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer
     2.6    uminus_rat.transfer times_rat.transfer inverse_rat.transfer
     2.7 -  positive.transfer of_rat.transfer
     2.8 +  positive.transfer of_rat.transfer rat.right_unique rat.right_total
     2.9  
    2.10  text {* De-register @{text "rat"} as a quotient type: *}
    2.11  

     3.1 --- a/src/HOL/RealDef.thy	Tue Feb 19 13:37:07 2013 +0100
     3.2 +++ b/src/HOL/RealDef.thy	Tue Feb 19 15:03:36 2013 +0100
     3.3 @@ -933,7 +933,8 @@
     3.4  lemmas [transfer_rule del] =
     3.5    real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer
     3.6    zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
     3.7 -  times_real.transfer inverse_real.transfer positive.transfer
     3.8 +  times_real.transfer inverse_real.transfer positive.transfer real.right_unique
     3.9 +  real.right_total
    3.10  
    3.11  subsection{*More Lemmas*}
    3.12