--- a/FSet.thy	Tue Oct 27 17:08:47 2009 +0100
+++ b/FSet.thy	Tue Oct 27 18:02:35 2009 +0100
@@ -426,28 +426,14 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done
 
-ML {* val (g, thm, othm) =
+ML {* val ind_r_t =
   Toplevel.program (fn () =>
-  repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+  repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
    @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
    (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
   )
 *}
-
-ML {*
-    fun tac2 ctxt =
-     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
-     THEN' (rtac othm); *}
-(* ML {*    val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1);
-*} *)
-
-ML {*
-  val ind_r_t2 =
-  Toplevel.program (fn () =>
-    repabs_eq2 @{context} (g, thm, othm)
-  )
-*}
-ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *}
+ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *}
 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"
   apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)
 done
@@ -468,11 +454,10 @@
 let
   val ind_r_a = atomize_thm thm;
   val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context};
-  val (g, t, ot) =
-    repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+  val ind_r_t =
+    repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
      @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
      (@{thms ho_memb_rsp ho_cons_rsp  ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs});
-  val ind_r_t = repabs_eq2 @{context} (g, t, ot);
   val ind_r_l = simp_lam_prs @{context} ind_r_t;
   val ind_r_a = simp_allex_prs @{context} quot ind_r_l;
   val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a;
@@ -490,10 +475,9 @@
 ML {* lift @{thm list_eq.intros(5)} *}
 ML {* lift @{thm card1_suc} *}
 ML {* lift @{thm map_append} *}
+(* ML {* lift @{thm append_assoc} *}*)
 
-(* ML {* lift @{thm append_assoc} *} *)
-
-thm 
+thm
 
 
 (*notation ( output) "prop" ("#_" [1000] 1000) *)