--- a/Nominal/FSet.thy	Mon Apr 19 11:55:12 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 12:20:18 2010 +0200
@@ -180,7 +180,7 @@
   apply (simp add: memb_def)
   done
 
-lemma mem_card_not_0:
+lemma memb_card_not_0:
   assumes a: "memb a A"
   shows "\<not>(fcard_raw A = 0)"
 proof -
@@ -195,10 +195,14 @@
   using a
   apply(induct xs arbitrary: ys)
   apply(auto simp add: memb_def)
-  apply(metis)
+  apply(subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
+  apply simp
+  apply auto
+  apply (drule_tac x="x" in spec)
+  apply blast
   apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
-  apply(simp add: fcard_raw_delete_one)
-  apply(metis Suc_pred'[OF fcard_raw_gt_0] fcard_raw_delete_one memb_def)
+  apply(simp add: fcard_raw_delete_one memb_def)
+  apply(metis Suc_pred'[OF fcard_raw_gt_0])
   done
 
 lemma fcard_raw_rsp[quot_respect]:
@@ -337,10 +341,15 @@
   apply (rule_tac [!] impI)
   apply (rule_tac [!] conjI)
   apply (rule_tac [!] impI)
-  apply (simp add: in_set_code memb_cons_iff memb_def)
-  apply (metis)
+  apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
+  apply (simp)
+  apply (simp add: memb_cons_iff memb_def)
+  apply auto
+  apply (drule_tac x="e" in spec)
+  apply blast
+  apply (simp add: memb_cons_iff)
   apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2)
-    length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))
+    length_Suc_conv memb_absorb nil_not_cons(2))
   apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
   apply (simp only:)
   apply (rule_tac f="f a1" in arg_cong)