--- a/QuotMain.thy	Thu Oct 15 11:57:33 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 12:06:00 2009 +0200
@@ -1058,16 +1058,16 @@
   apply (metis)
   done
 
-ML {* val li = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
+ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 
 prove card1_suc_r: {*
  Logic.mk_implies
-   ((prop_of li),
-   (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
+   ((prop_of card1_suc_f),
+   (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
   apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq])
   done
 
-ML {* @{thm card1_suc_r} OF [li] *}
+ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
 
 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}
 prove fold1_def_2_r: {*
@@ -1098,9 +1098,7 @@
 *}
 
 prove {* (Thm.term_of cgoal2) *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize(full))
-  apply (tactic {* transconv_fset_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} *})
   sorry
 
 ML {*
@@ -1110,7 +1108,7 @@
       val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs;
       val cgoal = cterm_of @{theory} goal;
       val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
-      val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (transconv_fset_tac' @{context}) 1;
+      val tac = transconv_fset_tac' @{context};
       val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
       val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
       val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
@@ -1136,15 +1134,14 @@
 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
-thm card1_suc_r
-(* ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc_r} @{context}) *}*)
-(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
-
 thm m1_lift
 thm leqi4_lift
 thm leqi5_lift
 thm m2_lift
-(*thm card_suc*)
+ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
+(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"}
+     (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*)
+(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
 
 thm leqi4_lift
 ML {*
@@ -1163,45 +1160,6 @@
   )
 *}
 
-(*
-thm card_suc
-ML {*
-  val (nam, typ) = hd (tl (Term.add_vars (prop_of @{thm card_suc})) [])
-  val (_, l) = dest_Type typ
-  val t = Type ("QuotMain.fset", l)
-  val v = Var (nam, t)
-  val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
-*}
-
-ML {*
-  Toplevel.program (fn () =>
-    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
-      Drule.instantiate' [] [SOME (cv)] @{thm card_suc}
-    )
-  )
-*}
-*)
-
-
-
-
-thm card1_suc
-
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc}))
-*}
-ML {*
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
-*}
-ML {* term_of @{cpat "all"} *}
-ML {*
-  val cgoal = 
-    Toplevel.program (fn () =>
-      cterm_of @{theory} goal
-    );
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
-*}
-
 lemma "(Ball (Respects ((op \<approx>) ===> (op =)))
          (((REP_fset ---> id) ---> id)
              (((ABS_fset ---> id) ---> id)
@@ -1236,6 +1194,7 @@
      (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))"
 thm APPLY_RSP
 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op =" "id" "id"]
+.
 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="])
 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
 thm LAMBDA_PRS1[symmetric]