--- a/src/HOL/Library/FSet.thy Thu Apr 10 17:48:14 2014 +0200
+++ b/src/HOL/Library/FSet.thy Thu Apr 10 17:48:15 2014 +0200
@@ -853,7 +853,7 @@
lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff)
-lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred]
+lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
subsubsection {* Quotient theorem for the Lifting package *}