--- a/FSet.thy	Wed Oct 28 16:16:38 2009 +0100
+++ b/FSet.thy	Wed Oct 28 16:48:57 2009 +0100
@@ -158,16 +158,15 @@
 term fold
 thm fold_def
 
-local_setup {*
-  old_make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn 
-  @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+where
+  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
 term map
 term fmap
 thm fmap_def
 
-
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
 

--- a/LamEx.thy	Wed Oct 28 16:16:38 2009 +0100
+++ b/LamEx.thy	Wed Oct 28 16:48:57 2009 +0100
@@ -53,7 +53,7 @@
 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 @{theory}) *}
+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 rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
@@ -77,94 +77,33 @@
 thm supp_def
 
 local_setup {*
-  make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
+  old_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 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_a = atomize_thm @{thm a3} *}
 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 *}
 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 *}
 ML {* val rr =  (add_lower_defs @{context} @{thms lperm_def}) *}
-ML {* val rrr = @{thm eq_reflection} OF [rr] *}
-ML {* MetaSimplifier.rewrite_rule [rrr] t_b *}
+ML {* val rrr = @{thm eq_reflection} OF [hd (rev rr)] *}
+lemma prod_fun_id: "prod_fun id id = id"
+  apply (simp add: prod_fun_def)
+done
+lemma map_id: "map id x = x"
+  apply (induct x)
+  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 {* ObjectLogic.rulify t_b' *}