--- a/FSet.thy	Mon Nov 02 09:47:49 2009 +0100
+++ b/FSet.thy	Mon Nov 02 11:15:26 2009 +0100
@@ -343,12 +343,17 @@
   apply (atomize(full))
   apply (tactic {* tac @{context} 1 *}) *)
 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *}
-ML {*
+(* ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 *}
-(*prove rg
+prove rg
 apply(atomize(full))
+ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
+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 {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done*)
 ML {* val ind_r_t =