--- a/FIXME-TODO	Thu Dec 10 16:56:03 2009 +0100
+++ b/FIXME-TODO	Thu Dec 10 18:28:30 2009 +0100
@@ -1,8 +1,10 @@
 Higher Priority
 ===============
 
-- redoing Int.thy (problem at the moment with overloaded
-  definitions....Florian)
+- handling constant definitions is ugly at the moment
+
+- if the constant definition gives the wrong definition
+  term, one gets a cryptic message about get_fun
 
 - have FSet.thy to have a simple infrastructure for 
   finite sets (syntax should be \<lbrace> \<rbrace>,
@@ -16,8 +18,6 @@
   And for examples where it is useful to lift types
   over a relation being only a partial equivalence
 
-
-
 - Handle theorems that include Ball/Bex
 
 - Test theorems with abstractions