--- a/FSet.thy	Mon Nov 02 11:15:26 2009 +0100
+++ b/FSet.thy	Mon Nov 02 11:51:50 2009 +0100
@@ -291,8 +291,8 @@
   by (simp add: fun_rel_id map_rsp)
 
 lemma map_append :
-  "(map f ((a::'a list) @ b)) \<approx>
-  ((map f a) ::'a list) @ (map f b)"
+  "(map f (a @ b)) \<approx>
+  (map f a) @ (map f b)"
  by simp (rule list_eq_refl)
 
 
@@ -318,7 +318,7 @@
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
-ML {* lift_thm_fset @{context} @{thm map_append} *}
+(*ML {* lift_thm_fset @{context} @{thm map_append} *}*)
 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
 
 thm fold1.simps(2)