diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -1405,7 +1405,7 @@
   apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> 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: if_split_asm)
+  apply (simp add: card_Diff_singleton_if split: if_split_asm)
   apply (case_tac "card A", auto)
   done