diff -r e749cefbf66c -r 973649d612f8 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Fri Jun 11 16:36:02 2010 +0200
+++ b/Nominal/FSet.thy	Fri Jun 11 17:52:06 2010 +0200
@@ -603,6 +603,8 @@
 is
   "concat"
 
+thm fconcat_def
+
 quotient_definition
   "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is