# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271678290 -7200
# Node ID b8cf69f0fe2f5c25c5ee9ab02a1e9850fe7ad70e
# Parent  edf10db61708c6088d994ddf1addd8800775430f
More cleaning

diff -r edf10db61708 -r b8cf69f0fe2f Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 12:28:48 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 13:58:10 2010 +0200
@@ -351,9 +351,8 @@
   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 nil_not_cons(2))
+  apply (case_tac b)
+  apply simp_all
   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)
@@ -364,8 +363,9 @@
   apply (erule memb_commute_ffold_raw)
   apply (drule_tac x="a1" in spec)
   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))
+  apply (simp add: memb_cons_iff)
+  apply (case_tac b)
+  apply simp_all
   done
 
 lemma [quot_respect]: