1.1 --- a/src/HOL/Lifting.thy	Wed Apr 18 10:52:49 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 18 12:15:20 2012 +0200
     1.3 @@ -341,6 +341,9 @@
     1.4  lemma typedef_right_total: "right_total T"
     1.5    unfolding right_total_def T_def by simp
     1.6  
     1.7 +lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
     1.8 +  unfolding fun_rel_def T_def by simp
     1.9 +
    1.10  lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
    1.11    unfolding T_def fun_rel_def
    1.12    by (metis type_definition.Rep [OF type]
    1.13 @@ -355,7 +358,7 @@
    1.14    "((T ===> op =) ===> op =)
    1.15      (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
    1.16    unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
    1.17 -  by (rule typedef_transfer_All [OF assms])
    1.18 +  by (rule typedef_transfer_All)
    1.19  
    1.20  end
    1.21  

     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 10:52:49 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 12:15:20 2012 +0200
     2.3 @@ -138,6 +138,8 @@
     2.4        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
     2.5          [[typedef_thm, T_def] MRSL @{thm typedef_right_total}])
     2.6        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
     2.7 +        [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
     2.8 +      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
     2.9          [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}])
    2.10        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.11          [[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}])