--- a/FSet.thy	Mon Nov 02 11:15:26 2009 +0100
+++ b/FSet.thy	Mon Nov 02 11:51:50 2009 +0100
@@ -291,8 +291,8 @@
   by (simp add: fun_rel_id map_rsp)
 
 lemma map_append :
-  "(map f ((a::'a list) @ b)) \<approx>
-  ((map f a) ::'a list) @ (map f b)"
+  "(map f (a @ b)) \<approx>
+  (map f a) @ (map f b)"
  by simp (rule list_eq_refl)
 
 
@@ -318,7 +318,7 @@
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
-ML {* lift_thm_fset @{context} @{thm map_append} *}
+(*ML {* lift_thm_fset @{context} @{thm map_append} *}*)
 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
 
 thm fold1.simps(2)

--- 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 *}