--- a/TODO	Thu Apr 08 11:50:30 2010 +0200
+++ b/TODO	Thu Apr 08 11:52:05 2010 +0200
@@ -39,8 +39,10 @@
   equivalence creates more than one permutation. According
   to the paper, this is incorrect.
 
-  Example in TestMorePerm.
+  Example in Classical.thy.
 
+- check whether weirdo example in TestMorePerm works
+  with shallow binders
 
 - nested recursion, like types "trm list" in a constructor