diff -r 09dff5ef8f74 -r f0a78fda343f FIXME-TODO
--- a/FIXME-TODO	Sat Dec 26 20:24:53 2009 +0100
+++ b/FIXME-TODO	Sat Dec 26 20:45:37 2009 +0100
@@ -10,35 +10,42 @@
 - clever code in quotiet_tacs.ML needs to be turned into
   boring code
 
-- comment about regularize tactic eeds to be adapted
+- comment about regularize tactic needs to be adapted
 
 - Check all the places where we do "handle _"
   (They make code changes very difficult: I sat 1/2
-  a day over simplification of calculate_inst before
+  a day over a simplification of calculate_inst before
   I understood things; the reason was that my exceptions
   where caught by the catch all. There is no problem
   with throwing and handling exceptions...it just must
-  be clear who throws what ad what is thrown.)
+  be clear who throws what and what is thrown.)
+
 
 Higher Priority
 ===============
 
-- if the constant definition gives the wrong definition
+- If the user defines twice the same quotient constant,
+  for example funion, then the line 
+
+    val Free (lhs_str, lhs_ty) = lhs
+
+  in quotient_def raises a bind exception.
+
+- If the constant definition gives the wrong definition
   term, one gets a cryptic message about absrep_fun
 
 - have FSet.thy to have a simple infrastructure for 
   finite sets (syntax should be \<lbrace> \<rbrace>,
   look at Set.thy how syntax is been introduced)
 
-- Handle theorems that include Ball/Bex. Would it help 
-  if we introduced separate Bex and Ball constants for 
-  quotienting?
+- Handle theorems that include Ball/Bex. For this, would 
+  it help if we introduced separate Bex and Ball constants 
+  for quotienting?
 
-- user should be able to give quotient_respects and 
+- The user should be able to give quotient_respects and 
   preserves theorems in a more natural form.
 
 
-
 Lower Priority
 ==============
 
@@ -55,22 +62,15 @@
 - inductions from the datatype package have a strange
   order of quantifiers in assumptions.
 
-- wrapper that translates an an original theorem given
-  a list of quotient_types as an attribute
+- wrapper for lifting ... to be used as an attribute
 
 - find clean ways how to write down the "mathematical"
   procedure for a possible submission (Peter submitted 
   his work only to TPHOLs 2005...we would have to go
   maybe for the Journal of Formalised Mathematics)
 
-- use lower-case letters where appropriate in order
-  to make Markus happy
-
 - add tests for adding theorems to the various thm lists
 
-- We shouldn't use the command 'quotient' as this shadows Larry's quotient.
-  Call it 'quotient_type'
-
 - Maybe quotient and equiv theorems like the ones for
   [QuotList, QuotOption, QuotPair...] could be automatically
   proven?