--- a/LamEx.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/LamEx.thy	Wed Oct 28 16:05:59 2009 +0100
@@ -73,14 +73,88 @@
 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_b *}
 
+thm fresh_def
+thm supp_def
+
 local_setup {*
-  make_const_def @{binding lfresh} @{term "fresh :: 'a \<Rightarrow> rlam \<Rightarrow> bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
   make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
 *}
 
-ML {* val consts = @{const_name fresh} :: @{const_name perm} :: consts *}
-ML {* val defs = @{thms lfresh_def lperm_def} @ defs *}
+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 t_u *}
+ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
+
+ML {*
+fun r_mk_comb_tac_lam ctxt = r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms
+*}
+
+prove {* build_repabs_goal @{context} t_r consts rty qty *}
+apply (atomize(full))
+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 {* (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 *})
+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 {* (r_mk_comb_tac_lam @{context}) 1 *})
+nitpick
+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 *})
+
+
+
+
+
+
+
 ML {* val t_t = Toplevel.program (fn () => repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms) *}
+
+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 *}
@@ -94,7 +168,11 @@
 
 
 
-
+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