--- a/src/HOL/Library/FSet.thy Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Library/FSet.thy Tue Jan 22 12:00:16 2019 +0000
@@ -236,8 +236,8 @@
lemmas contra_fsubsetD[no_atp] = contra_subsetD[Transfer.transferred]
lemmas fsubset_refl = subset_refl[Transfer.transferred]
lemmas fsubset_trans = subset_trans[Transfer.transferred]
-lemmas fset_rev_mp = set_rev_mp[Transfer.transferred]
-lemmas fset_mp = set_mp[Transfer.transferred]
+lemmas fset_rev_mp = rev_subsetD[Transfer.transferred]
+lemmas fset_mp = subsetD[Transfer.transferred]
lemmas fsubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred]
lemmas eq_fmem_trans = eq_mem_trans[Transfer.transferred]
lemmas fsubset_antisym[intro!] = subset_antisym[Transfer.transferred]