--- a/FIXME-TODO	Sun Jan 24 23:41:27 2010 +0100
+++ b/FIXME-TODO	Mon Jan 25 17:53:08 2010 +0100
@@ -1,19 +1,9 @@
 Highest Priority
 ================
 
-- better lookup mechanism for quotient definition
-  (see fixme in quotient_term.ML)
-
 Higher Priority
 ===============
 
-- 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