diff -r 38810e1df801 -r fcff14e578d3 FSet.thy
--- a/FSet.thy	Thu Oct 29 07:29:12 2009 +0100
+++ b/FSet.thy	Thu Oct 29 08:06:49 2009 +0100
@@ -177,7 +177,7 @@
 term fmap
 thm fmap_def
 
-ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def card_def INSERT_def fmap_def fold_def} *}
+ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def fold_def} *}
 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
 
 ML {*
@@ -187,7 +187,6 @@
                 @{const_name "map"}];
 *}
 
-(* FIXME: does not work anymore :o( *)
 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
 lemma memb_rsp:
@@ -315,7 +314,7 @@
   @ @{thms ho_all_prs ho_ex_prs} *}
 ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *}
 ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *}
-ML {* val defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
+ML {* val defs = fset_defs *}
 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
 ML {*
   val consts = [@{const_name "Nil"}, @{const_name "Cons"},