--- a/FSet.thy	Sat Nov 28 05:29:30 2009 +0100
+++ b/FSet.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -307,8 +307,7 @@
 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
 
 lemma "IN x EMPTY = False"
-apply (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
-done
+by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
 
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})