--- a/QuotMain.thy	Thu Sep 24 09:09:46 2009 +0200
+++ b/QuotMain.thy	Thu Sep 24 11:38:20 2009 +0200
@@ -856,7 +856,7 @@
 
 ML {*
   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
-  val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}]
+  val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}]
 *}
 
 ML {*
@@ -870,6 +870,7 @@
       in
         if type_of t = lifted_type then mk_rep_abs t else t
       end
+      handle TYPE _ => t
     fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
       | build_aux (f $ a) =
           let
@@ -1084,7 +1085,15 @@
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false 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 (rule_tac f = "P" in arg_cong)
+  sorry
 
 thm card1_suc
 
@@ -1098,6 +1107,8 @@
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
+prove {* (Thm.term_of cgoal2) *}
+  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )