--- a/FSet.thy	Fri Oct 30 18:31:06 2009 +0100
+++ b/FSet.thy	Fri Oct 30 19:03:53 2009 +0100
@@ -322,28 +322,24 @@
 thm list.recs(2)
 thm list.cases
 
-
-ML {* val ind_r_a = atomize_thm @{thm m2} *}
-prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
-  ML_prf {*  fun tac ctxt =
+ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
+(* prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
+ ML_prf {*  fun tac ctxt =
      (FIRST' [
       rtac rel_refl,
       atac,
-      (rtac @{thm  allI} THEN' dtac @{thm spec}),
+      rtac @{thm get_rid},
+      rtac @{thm get_rid2},
       (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
-      MetisTools.metis_tac ctxt [],
-      rtac (@{thm eq_rr} OF [rel_refl]),
-      ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]))
+      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
+      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
     ]);
  *}
-  apply (tactic {* tac @{context} 1 *}) 
-  apply (tactic {* tac @{context} 1 *}) 
-  apply (tactic {* tac @{context} 1 *}) 
-
-
-ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *}
+  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 {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);