diff -r f189cf2c0987 -r 24ae81462f3e Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 21 21:29:09 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 21:31:07 2010 +0200
@@ -589,6 +589,8 @@
   apply (simp_all)
   apply (case_tac "memb a A")
   apply (auto simp add: memb_def)[2]
+  apply (case_tac "list_eq2 (a # A) A")
+  apply (metis list_eq2.intros(3) list_eq2.intros(6))
   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
   apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)