--- a/QuotMain.thy	Thu Sep 24 11:38:20 2009 +0200
+++ b/QuotMain.thy	Thu Sep 24 13:32:52 2009 +0200
@@ -887,13 +887,8 @@
   Logic.mk_equals ((build_aux concl2), concl2)
 end *}
 
-ML {* val emptyt = (symmetric (unlam_def  @{context} @{thm EMPTY_def})) *}
-ML {* val in_t = (symmetric (unlam_def  @{context} @{thm IN_def})) *}
-ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *}
-ML {* val cardt =  symmetric (unlam_def @{context} @{thm card_def}) *}
-ML {* val insertt =  symmetric (unlam_def @{context} @{thm INSERT_def}) *}
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
-ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *}
+ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *}
 
 ML {*
   fun dest_cbinop t =
@@ -962,6 +957,7 @@
       rtac @{thm list_eq_sym},
       rtac @{thm cons_preserves},
       rtac @{thm mem_respects},
+      rtac @{thm card1_rsp},
       rtac @{thm QUOT_TYPE_I_fset.R_trans2},
       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
       foo_tac,
@@ -1062,7 +1058,7 @@
     )
 *}
 ML {*
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
@@ -1083,15 +1079,12 @@
 *}
 ML {*
   val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 ML fset_defs_sym
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize(full))
-  apply (rule_tac trueprop_cong)
-  apply (atomize(full))
-  apply (tactic {* foo_tac' @{context} 1 *}) 
+  apply (tactic {* foo_tac' @{context} 1 *})
   apply (rule_tac f = "P" in arg_cong)
   sorry
 
@@ -1105,10 +1098,11 @@
 *}
 ML {*
   val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (tactic {* foo_tac' @{context} 1 *})