diff -r 8cf5c3e58889 -r 8ed62410236e Nominal/Ex/Datatypes.thy
--- a/Nominal/Ex/Datatypes.thy	Fri Nov 05 15:21:10 2010 +0000
+++ b/Nominal/Ex/Datatypes.thy	Sat Nov 06 06:18:41 2010 +0000
@@ -7,6 +7,7 @@
   atom_decl - example by John Matthews
 *)
 
+(* FIXME: throws an problem with fv-function
 nominal_datatype 'a Maybe = 
   Nothing 
 | Just 'a
@@ -22,6 +23,7 @@
 thm Maybe.fv_bn_eqvt
 thm Maybe.size_eqvt
 thm Maybe.supp
+*)
 
 (*
   using a datatype inside a nominal_datatype