--- a/FSet.thy	Sat Nov 28 05:09:22 2009 +0100
+++ b/FSet.thy	Sat Nov 28 05:47:13 2009 +0100
@@ -445,6 +445,7 @@
   done
 
 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun r_mk_comb_tac_fset' lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
@@ -462,6 +463,8 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)