--- a/src/HOL/Library/Countable_Set_Type.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Tue Feb 23 16:25:08 2016 +0100
@@ -219,8 +219,8 @@
lemmas cimage_csubset_iff[no_atp] = image_subset_iff[Transfer.transferred]
lemmas cimage_csubsetI = image_subsetI[Transfer.transferred]
lemmas cimage_ident[simp] = image_ident[Transfer.transferred]
-lemmas split_if_cin1 = split_if_mem1[Transfer.transferred]
-lemmas split_if_cin2 = split_if_mem2[Transfer.transferred]
+lemmas if_split_cin1 = if_split_mem1[Transfer.transferred]
+lemmas if_split_cin2 = if_split_mem2[Transfer.transferred]
lemmas cpsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred]
lemmas cpsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred]
lemmas cpsubset_finsert_iff = psubset_insert_iff[Transfer.transferred]