# HG changeset patch
# User kuncar
# Date 1397144893 -7200
# Node ID 7e8a369eb10d36e250fa744a626c343289869a3c
# Parent  a13c2ccc160b7622642b0e0e38dd9bc4699df0e3
tuned

diff -r a13c2ccc160b -r 7e8a369eb10d src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Thu Apr 10 15:14:38 2014 +0200
+++ b/src/HOL/Lifting.thy	Thu Apr 10 17:48:13 2014 +0200
@@ -48,9 +48,9 @@
   where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
 
 lemma left_unique_transfer [transfer_rule]:
-  assumes [transfer_rule]: "right_total A"
-  assumes [transfer_rule]: "right_total B"
-  assumes [transfer_rule]: "bi_unique A"
+  assumes "right_total A"
+  assumes "right_total B"
+  assumes "bi_unique A"
   shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
 using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
 by metis