--- a/LamEx.thy	Mon Nov 02 11:15:26 2009 +0100
+++ b/LamEx.thy	Mon Nov 02 11:51:50 2009 +0100
@@ -240,7 +240,7 @@
  *}
   apply (tactic {* tac @{context} 1 *}) *)
 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
-ML {*
+(*ML {*
   val rt = build_repabs_term @{context} t_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 *}
@@ -259,7 +259,6 @@
     ),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     rtac refl,
-(*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
     (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
     Cong_Tac.cong_tac @{thm cong},
     rtac @{thm ext},
@@ -274,45 +273,18 @@
   fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
 *}
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-prefer 2
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
-
+*)
 
 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
+
+ML {*
+
+
+*}
+
 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *}
 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}