--- a/FSet.thy	Sat Nov 28 08:46:24 2009 +0100
+++ b/FSet.thy	Sat Nov 28 13:54:48 2009 +0100
@@ -328,9 +328,11 @@
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 done
 
-lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) =
+ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+
+lemma "FOLD f g (z::'b) (INSERT a x) =
   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
-apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
+apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
@@ -341,8 +343,6 @@
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done
 
-ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
-
 lemma cheat: "P" sorry
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"