# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308733035 -32400
# Node ID 0599286b1e2a025bdc0bf9245eda548ccdd0df77
# Parent  05a4745b0a9d86cb5fa3eb89fffba465c52e255e
constants with the same names

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
 ==============