--- a/FSet.thy	Wed Nov 25 15:43:12 2009 +0100
+++ b/FSet.thy	Wed Nov 25 21:48:32 2009 +0100
@@ -304,7 +304,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 ML {* val consts = lookup_quot_consts defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
 
 lemma "IN x EMPTY = False"
 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
@@ -334,8 +334,6 @@
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
-apply(tactic {* Induct.fix_tac @{context} 0 [("x", @{typ "'b fset"}), ("xa", @{typ "'b fset"})] 1 *})
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done
 
@@ -343,12 +341,8 @@
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done
 
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 done
 
 quotient_def
@@ -376,26 +370,14 @@
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
 
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* (simp_tac (HOL_ss addsimps
-  @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 1 *})
-ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 done
 
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 done
 
 lemma list_induct_part:
@@ -416,7 +398,7 @@
 
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *})
+apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
@@ -442,7 +424,6 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule IDENTITY_QUOTIENT)
 apply (rule FUN_QUOTIENT)
@@ -467,7 +448,6 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
 apply assumption
 apply (rule refl)
@@ -486,14 +466,7 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (simp only:map_id)
-apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
-ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
-apply (tactic {* lambda_prs_tac @{context} quot 1 *})
-ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'c list \<Rightarrow> bool)"} *}
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
 done
 
 end