--- a/FIXME-TODO	Wed Jan 13 16:23:32 2010 +0100
+++ b/FIXME-TODO	Wed Jan 13 16:39:20 2010 +0100
@@ -4,23 +4,6 @@
 - better lookup mechanism for quotient definition
   (see fixme in quotient_term.ML)
 
-- check needs to be fixed in mk_resp_arg (quotient_term.ML),
-  see test for (_, Const _)
-
-- clever code in quotiet_tacs.ML needs to be turned into
-  boring code
-
-- 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 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 and what is thrown.)
-
-
 Higher Priority
 ===============
 
@@ -34,10 +17,6 @@
 - 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. For this, would 
   it help if we introduced separate Bex and Ball constants 
   for quotienting?
@@ -49,10 +28,6 @@
 Lower Priority
 ==============
 
-- Maybe a quotient_definition should already require
-  a proof of the respectfulness (in this way one
-  already excludes non-sensical definitions)
-
 - accept partial equivalence relations
 
 - think about what happens if things go wrong (like