diff -r e965524c3301 -r 003c7e290a04 Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 15:07:27 2010 +0100
@@ -68,22 +68,20 @@
 
 text {* example type schemes *}
 
-(* does not work yet 
-nominal_datatype t = 
-  Var "name" 
+(* does not work yet
+nominal_datatype t =
+  Var "name"
 | Fun "t" "t"
 
-nominal_datatype tyS = 
+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 *)
 
@@ -137,12 +135,12 @@
 
 (* example 4 from Terms.thy *)
 
-(* does not work yet
+
 nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 x::"name" t::"trm4"  bind x in t
-*)
+
 
 (* example 5 from Terms.thy *)