1.1 --- a/src/HOL/Lifting.thy	Thu Apr 10 15:14:38 2014 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Apr 10 17:48:13 2014 +0200
     1.3 @@ -48,9 +48,9 @@
     1.4    where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
     1.5  
     1.6  lemma left_unique_transfer [transfer_rule]:
     1.7 -  assumes [transfer_rule]: "right_total A"
     1.8 -  assumes [transfer_rule]: "right_total B"
     1.9 -  assumes [transfer_rule]: "bi_unique A"
    1.10 +  assumes "right_total A"
    1.11 +  assumes "right_total B"
    1.12 +  assumes "bi_unique A"
    1.13    shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
    1.14  using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
    1.15  by metis