diff -r 9761840f2d5c -r b2fa5de30a73 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 11:38:43 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 11:55:12 2010 +0200
@@ -183,7 +183,11 @@
 lemma mem_card_not_0:
   assumes a: "memb a A"
   shows "\<not>(fcard_raw A = 0)"
-  by (metis a fcard_raw_0 none_memb_nil)
+proof -
+  have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
+  then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
+  then show ?thesis using fcard_raw_0[of A] by simp
+qed
 
 lemma fcard_raw_rsp_aux:
   assumes a: "xs \<approx> ys"
@@ -343,7 +347,7 @@
   apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
   apply simp
   apply (simp add: memb_delete_raw)
-  apply (metis memb_cons_iff)
+  apply (auto simp add: memb_cons_iff)[1]
   apply (erule memb_commute_ffold_raw)
   apply (drule_tac x="a1" in spec)
   apply (simp add: memb_cons_iff)