diff -r 05a4745b0a9d -r 0599286b1e2a Attic/FIXME-TODO
--- a/Attic/FIXME-TODO	Wed Jun 22 04:49:56 2011 +0900
+++ b/Attic/FIXME-TODO	Wed Jun 22 17:57:15 2011 +0900
@@ -24,6 +24,11 @@
     typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
       morphisms list_of_dlist Abs_dlist
 
+- Allow defining constants with existing names.
+    Since 'insert' is defined for sets,
+    "quotient_definition insert" fails for fset
+    however "definition" succeeds.
+
 Lower Priority
 ==============