
diff -r acbf50e8eac2 -r 9c968284553c Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Mon Feb 22 10:39:05 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 10:57:39 2010 +0100
@@ -90,6 +90,8 @@
 
 *}
 
+(* TODO: Notice datatypes without bindings and replace alpha with equality *)
+
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
 fun define_fv_alpha full_tname bindsall lthy =




