--- a/FSet.thy	Fri Dec 04 18:32:19 2009 +0100
+++ b/FSet.thy	Fri Dec 04 19:06:53 2009 +0100
@@ -297,6 +297,10 @@
 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
 lemma "IN x EMPTY = False"
+
+apply(tactic {* (ObjectLogic.full_atomize_tac
+  THEN' gen_frees_tac @{context}) 1 *})
+
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})