diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/FSet.thy	Fri May 13 20:24:10 2016 +0200
@@ -855,7 +855,7 @@
 
 lemma bind_transfer [transfer_rule]:
   "(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind"
-  using assms unfolding rel_fun_def
+  unfolding rel_fun_def
   using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close>
@@ -885,7 +885,7 @@
 
 lemma fSup_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup"
-  using assms unfolding rel_fun_def
+  unfolding rel_fun_def
   apply clarify
   apply transfer'
   using Sup_fset_transfer[unfolded rel_fun_def] by blast
@@ -908,7 +908,7 @@
 
 lemma card_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard"
-  using assms unfolding rel_fun_def
+  unfolding rel_fun_def
   using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 end