--- a/FSet.thy	Wed Nov 04 10:43:33 2009 +0100
+++ b/FSet.thy	Wed Nov 04 11:08:05 2009 +0100
@@ -333,7 +333,7 @@
 term list_rec
 
 quotient_def
-  fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'b"
+  fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
   "fset_rec \<equiv> list_rec"
 
@@ -351,8 +351,8 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
 
 
-ML {* val ind_r_a = atomize_thm @{thm card1_suc} *}
-(* prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
+ML {* val ind_r_a = atomize_thm @{thm map_append} *}
+ prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
  ML_prf {*  fun tac ctxt =
      (FIRST' [
       rtac rel_refl,