--- a/LamEx.thy	Thu Nov 05 13:47:41 2009 +0100
+++ b/LamEx.thy	Thu Nov 05 16:43:57 2009 +0100
@@ -259,7 +259,7 @@
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
 
-ML {* val t_a = atomize_thm @{thm alpha.induct} *}
+ML {* val t_a = atomize_thm @{thm alpha.cases} *}
 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
 ML_prf {*  fun tac ctxt =
      (FIRST' [
@@ -278,13 +278,13 @@
   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);
 *}
 prove rg
 apply(atomize(full))
-ML_prf {*
+(*ML_prf {*
 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
   (FIRST' [
     rtac trans_thm,
@@ -308,10 +308,37 @@
     ),
     WEAK_LAMBDA_RES_TAC ctxt
     ]);
+*}*)
+ML_prf {*
   fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
 *}
+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 {* (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 *})
-*)
+
 
 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})) *}