changeset 1206 | 9c968284553c |
parent 1199 | 5770c73f2415 |
child 1207 | fb33684e4ece |
--- 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 =