# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271672928 -7200
# Node ID edf10db61708c6088d994ddf1addd8800775430f
# Parent  5fd2ed81514427a7d78e8f9d816c76d184940c89
remove more metis

diff -r 5fd2ed815144 -r edf10db61708 Nominal/FSet.thy
--- 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]: