--- a/FSet.thy	Thu Nov 05 10:46:54 2009 +0100
+++ b/FSet.thy	Thu Nov 05 13:47:04 2009 +0100
@@ -172,6 +172,8 @@
 term fmap
 thm fmap_def
 
+ML {* prop_of @{thm fmap_def} *}
+
 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val defs_sym = add_lower_defs @{context} defs *}