--- a/LamEx.thy	Fri Oct 30 11:25:29 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 12:22:03 2009 +0100
@@ -124,34 +124,19 @@
   apply(simp add: abs_fresh)
   done
 
-ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def} *}
-ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}, @{const_name "perm"}]; *}
 
-ML {* val rty = @{typ "rlam"} *}
 ML {* val qty = @{typ "lam"} *}
-ML {* val rel = @{term "alpha"} *}
-ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *}
-ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *}
-ML {* val quot = @{thm QUOTIENT_lam} *}
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def} *}
+ML {* val consts = lookup_quot_consts defs *}
+ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "lam" *}
 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
-ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *}
-ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *}
-
-ML {* add_lower_defs @{context} @{thms perm_lam_def} *}
-ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms perm_lam_def}))] *}
-
-ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} 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 {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *}
 
 ML {* lift_thm_lam @{context} @{thm pi_var_com} *}
 ML {* lift_thm_lam @{context} @{thm pi_app_com} *}
 ML {* lift_thm_lam @{context} @{thm pi_lam_com} *}
 
-thm supp_def
-
 fun
   option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
 where
@@ -182,7 +167,7 @@
   (* Simp starts hanging so don't know how to continue *)
   sorry
 
-(* Christian: Does it make sense? *)
+(* Not sure if it make sense or if it will be needed *)
 lemma abs_fun_rsp: "(op = ===> alpha ===> op = ===> op =) abs_fun abs_fun"
 sorry
 
@@ -216,10 +201,7 @@
 sorry
 
 ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *}
-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 {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *}
 
 thm a3
 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *}