
diff -r 29800666e526 -r 842917225d56 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Library/FSet.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -300,8 +300,8 @@
 lemmas fimage_fsubset_iff[no_atp] = image_subset_iff[Transfer.transferred]
 lemmas fimage_fsubsetI = image_subsetI[Transfer.transferred]
 lemmas fimage_ident[simp] = image_ident[Transfer.transferred]
-lemmas split_if_fmem1 = split_if_mem1[Transfer.transferred]
-lemmas split_if_fmem2 = split_if_mem2[Transfer.transferred]
+lemmas if_split_fmem1 = if_split_mem1[Transfer.transferred]
+lemmas if_split_fmem2 = if_split_mem2[Transfer.transferred]
 lemmas pfsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred]
 lemmas pfsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred]
 lemmas pfsubset_finsert_iff = psubset_insert_iff[Transfer.transferred]




