--- a/FSet.thy	Tue Nov 03 14:04:45 2009 +0100
+++ b/FSet.thy	Tue Nov 03 16:17:19 2009 +0100
@@ -309,9 +309,6 @@
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
-lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
-by (simp add: list_eq_refl)
-
 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
@@ -320,6 +317,7 @@
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
 (*ML {* lift_thm_fset @{context} @{thm map_append} *}*)
 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
+ML {* lift_thm_fset @{context} @{thm list.induct} *}
 
 thm fold1.simps(2)
 thm list.recs(2)
@@ -343,17 +341,13 @@
   apply (atomize(full))
   apply (tactic {* tac @{context} 1 *}) *)
 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *}
-(* ML {*
+(*ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 *}
 prove rg
 apply(atomize(full))
 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
-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 {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done*)
 ML {* val ind_r_t =
@@ -365,6 +359,8 @@
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
+thm APP_PRS
+ML aps
 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *}
 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *}