--- a/FSet.thy	Tue Dec 01 12:16:45 2009 +0100
+++ b/FSet.thy	Tue Dec 01 14:04:00 2009 +0100
@@ -523,4 +523,7 @@
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 done
 
+ML {* #quot_thm (hd (quotdata_dest @{theory})) *}
+print_quotients
+thm QUOTIENT_fset
 end