--- a/Nominal/FSet.thy	Mon Apr 19 12:20:18 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 12:28:48 2010 +0200
@@ -202,7 +202,11 @@
   apply blast
   apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
   apply(simp add: fcard_raw_delete_one memb_def)
-  apply(metis Suc_pred'[OF fcard_raw_gt_0])
+  apply (case_tac "a \<in> set ys")
+  apply (simp only: if_True)
+  apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
+  apply (drule Suc_pred'[OF fcard_raw_gt_0])
+  apply auto
   done
 
 lemma fcard_raw_rsp[quot_respect]: