# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271669923 -7200
# Node ID 9761840f2d5c690c3ee7de101157456a5ff180a8
# Parent  a3db645bbfdad8e1d688a46c285998b401b2f14f# Parent  d360a26fa790ccacb97e52ff6f2636526081358f
merge

diff -r d360a26fa790 -r 9761840f2d5c Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 09:27:53 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 11:38:43 2010 +0200
@@ -335,10 +335,7 @@
   apply (rule_tac [!] impI)
   apply (simp add: in_set_code memb_cons_iff memb_def)
   apply (metis)
-  apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) 
-    length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))
-  defer
-  apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) 
+  apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2)
     length_Suc_conv memb_absorb memb_cons_iff 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:)
@@ -350,6 +347,8 @@
   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))
   done
 
 lemma [quot_respect]: