--- a/FIXME-TODO	Tue Dec 22 21:44:50 2009 +0100
+++ b/FIXME-TODO	Tue Dec 22 22:10:48 2009 +0100
@@ -1,8 +1,30 @@
+Highest Priority
+================
+
+- 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 eeds 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
+  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.)
+
 Higher Priority
 ===============
 
 - if the constant definition gives the wrong definition
-  term, one gets a cryptic message about get_fun
+  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>,
@@ -15,7 +37,7 @@
 - user should be able to give quotient_respects and 
   preserves theorems in a more natural form.
 
-- the test in the (_, Const _) needs to be fixed
+
 
 Lower Priority
 ==============
@@ -24,7 +46,7 @@
   a proof of the respectfulness (in this way one
   already excludes non-sensical definitions)
 
-- accept partial equvalence relations
+- accept partial equivalence relations
 
 - think about what happens if things go wrong (like
   theorem cannot be lifted) / proper diagnostic 
@@ -46,9 +68,6 @@
 
 - add tests for adding theorems to the various thm lists
 
-
-- Check all the places where we do "handle _"
-
 - We shouldn't use the command 'quotient' as this shadows Larry's quotient.
   Call it 'quotient_type'