--- a/FSet.thy	Fri Oct 30 16:37:09 2009 +0100
+++ b/FSet.thy	Fri Oct 30 18:31:06 2009 +0100
@@ -316,22 +316,33 @@
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
 ML {* lift_thm_fset @{context} @{thm map_append} *}
-ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *}
+ML {* lift_thm_fset @{context} @{thm append_assoc} *}
 
 thm fold1.simps(2)
 thm list.recs(2)
 thm list.cases
 
 
-ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
-(*prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
+ML {* val ind_r_a = atomize_thm @{thm m2} *}
+prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
   ML_prf {*  fun tac ctxt =
-       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+     (FIRST' [
+      rtac rel_refl,
+      atac,
+      (rtac @{thm  allI} THEN' dtac @{thm spec}),
+      (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])])) THEN_ALL_NEW
-         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
-         (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *}
-  apply (tactic {* tac @{context} 1 *})*)
+         (@{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]))
+    ]);
+ *}
+  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} *}
 ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty