--- a/LamEx.thy	Wed Oct 28 17:17:21 2009 +0100
+++ b/LamEx.thy	Wed Oct 28 17:38:37 2009 +0100
@@ -60,21 +60,11 @@
 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *}
 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *}
 
-thm a3
-ML {* val t_a = atomize_thm @{thm a3} *}
-ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
-ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
-ML {* val abs = findabs rty (prop_of t_a) *}
-ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
-ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
-ML {* val t_c = simp_allex_prs @{context} quot t_l *}
-ML {* val t_defs_sym = add_lower_defs @{context} defs *}
-ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *}
-ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *}
-ML {* ObjectLogic.rulify t_b *}
-
-thm fresh_def
-thm supp_def
+ML {*
+fun lift_thm_lam lthy t =
+  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
+*}
+ML {* lift_thm_lam @{context} @{thm a3} *}
 
 local_setup {*
   old_make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
@@ -82,17 +72,12 @@
 
 ML {* val consts = @{const_name perm} :: consts *}
 ML {* val defs = @{thms lperm_def} @ defs *}
-ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *}
-ML {* val t_a = atomize_thm @{thm a3} *}
-ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
-ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
-ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
-ML {* val t_c = simp_allex_prs @{context} quot t_l *}
-ML {* val t_defs_sym = add_lower_defs @{context} defs *}
-ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *}
-ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *}
-ML {* val rr =  (add_lower_defs @{context} @{thms lperm_def}) *}
-ML {* val rrr = @{thm eq_reflection} OF [hd (rev rr)] *}
+ML {*
+fun lift_thm_lam lthy t =
+  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
+*}
+ML {* val t_b = lift_thm_lam @{context} @{thm a3} *}
+ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms lperm_def}))] *}
 lemma prod_fun_id: "prod_fun id id = id"
   apply (simp add: prod_fun_def)
 done
@@ -101,21 +86,12 @@
   apply (simp_all add: map.simps)
 done
 
-ML {* val rrrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rrr *}
-ML {* val t_b' = eqsubst_thm @{context} [rrrr] t_b *}
+ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *}
+ML {* val t_b' = eqsubst_thm @{context} [rrr] (atomize_thm t_b) *}
 ML {* ObjectLogic.rulify t_b' *}
 
-
+ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *}
+lemma "alpha ===> (alpha ===> op =) op = op ="
+sorry
 
-local_setup {*
-  make_const_def @{binding lfresh} @{term "fresh :: 'a \<Rightarrow> rlam \<Rightarrow> bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
-*}
-@{const_name fresh} :: 
-lfresh_def 
-ML {*
-fun lift_thm_lam lthy t =
-  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
-*}
-
-ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *}
-
+ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *)