--- a/Nominal/Test.thy	Tue Mar 02 14:24:57 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 14:51:40 2010 +0100
@@ -68,22 +68,20 @@
 
 text {* example type schemes *}
 
+(* does not work yet
 nominal_datatype t =
   Var "name"
 | Fun "t" "t"
 
-(* does not work yet
 nominal_datatype tyS =
   All xs::"name list" ty::"t_raw" bind xs in ty
 *)
 
-(* also does not work
 nominal_datatype t = 
   Var "name" 
 | Fun "t" "t"
 and  tyS = 
-  All xs::"name list" ty::"t" bind xs in ty
-*)
+  All xs::"name set" ty::"t" bind xs in ty
 
 (* example 1 from Terms.thy *)