--- a/FSet.thy	Fri Dec 04 19:06:53 2009 +0100
+++ b/FSet.thy	Fri Dec 04 19:47:58 2009 +0100
@@ -297,10 +297,6 @@
 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 *})