--- a/FSet.thy	Thu Nov 12 12:07:33 2009 +0100
+++ b/FSet.thy	Thu Nov 12 13:56:07 2009 +0100
@@ -305,6 +305,9 @@
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
+thm m2
+
+thm append_assoc
 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}