diff -r 1d6a0aeef4a1 -r faa7e6033f2e Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 14 08:36:54 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 14 08:42:38 2010 +0200
@@ -483,8 +483,6 @@
   "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
   by (lifting set.simps)
 
-thm memb_def[symmetric, THEN meta_eq_to_obj_eq]
-
 lemma in_fset_to_set:
   "x \<in> fset_to_set S \<equiv> x |\<in>| S"
   by (lifting memb_def[symmetric])