--- a/FSet.thy	Tue Oct 27 18:02:35 2009 +0100
+++ b/FSet.thy	Tue Oct 27 18:05:45 2009 +0100
@@ -468,6 +468,9 @@
 *}
 ML fset_defs
 
+lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
+by (simp add: list_eq_refl)
+
 
 ML {* lift @{thm m2} *}
 ML {* lift @{thm m1} *}
@@ -475,7 +478,7 @@
 ML {* lift @{thm list_eq.intros(5)} *}
 ML {* lift @{thm card1_suc} *}
 ML {* lift @{thm map_append} *}
-(* ML {* lift @{thm append_assoc} *}*)
+ML {* lift @{thm eq_r[OF append_assoc]} *}
 
 thm