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 =