--- a/FSet.thy	Thu Dec 03 11:58:46 2009 +0100
+++ b/FSet.thy	Thu Dec 03 12:17:23 2009 +0100
@@ -481,4 +481,8 @@
 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
 done
 
+ML {* qconsts_lookup @{theory} "EMPTY" *}
+thm EMPTY_def
+
+
 end