src/HOL/Library/FSet.thy

   using rel_set_transfer[unfolded rel_fun_def,rule_format, Transfer.transferred, where A = A and B = B]
   by simp
 
 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>
 
 lemma fmember_transfer [transfer_rule]:

   using assms unfolding rel_fun_def
   using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 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
 
 (* FIXME: add right_total_fInf_transfer *)

   using assms unfolding rel_fun_def
   using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 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
 
 lifting_update fset.lifting