Nominal/Ex/Datatypes.thy
changeset 2557 781fbc8c0591
parent 2556 8ed62410236e
child 2559 add799cf0817
--- a/Nominal/Ex/Datatypes.thy	Sat Nov 06 06:18:41 2010 +0000
+++ b/Nominal/Ex/Datatypes.thy	Sun Nov 07 11:22:31 2010 +0000
@@ -7,7 +7,7 @@
   atom_decl - example by John Matthews
 *)
 
-(* FIXME: throws an problem with fv-function
+
 nominal_datatype 'a Maybe = 
   Nothing 
 | Just 'a
@@ -23,7 +23,6 @@
 thm Maybe.fv_bn_eqvt
 thm Maybe.size_eqvt
 thm Maybe.supp
-*)
 
 (*
   using a datatype inside a nominal_datatype