--- a/Nominal/Ex/TypeVarsTest.thy	Tue Feb 19 05:38:46 2013 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Tue Feb 19 06:58:14 2013 +0000
@@ -17,9 +17,9 @@
 instance nat :: s1 ..
 instance int :: s2 .. 
 
-nominal_datatype ('a::s1, 'b::s2, 'c::at) lam =
+nominal_datatype ('a, 'b, 'c) lam =
   Var "name"
-| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
+| App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam"
 | Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
 | Foo "'a" "'b"
 | Bar x::"'c" l::"('a, 'b, 'c) lam"  binds x in l   (* Bar binds a polymorphic atom *)
@@ -44,15 +44,6 @@
 | Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
 
 
-nominal_datatype 'a foo = 
-  Node x::"name" f::"'a foo" binds x in f
-| Leaf "'a"
-
-term "Leaf"
-
-
-
-
 end