diff -r 29800666e526 -r 842917225d56 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -1312,7 +1312,7 @@
 apply (subgoal_tac "finite A & A - {x} <= F")
  prefer 2 apply (blast intro: finite_subset, atomize)
 apply (drule_tac x = "A - {x}" in spec)
-apply (simp add: card_Diff_singleton_if split add: split_if_asm)
+apply (simp add: card_Diff_singleton_if split add: if_split_asm)
 apply (case_tac "card A", auto)
 done