diff -r 94ed05fb090e -r 6c5e3ac737d9 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 21 13:39:34 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 19:10:55 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)