diff -r 19f5e7afad89 -r 578e0265b235 Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Thu Dec 22 04:35:01 2011 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Thu Dec 22 13:10:30 2011 +0000
@@ -17,7 +17,7 @@
 instance nat :: s1 ..
 instance int :: s2 .. 
 
-nominal_datatype ('a::"{s1,fs}", 'b::"{s2,fs}", 'c::at) lam =
+nominal_datatype ('a::s1, 'b::s2, 'c::at) lam =
   Var "name"
 | App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
 | Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
@@ -41,11 +41,11 @@
 
 nominal_datatype ('alpha, 'beta, 'gamma) psi =
   PsiNil
-| Output "'alpha::fs" "'alpha::fs" "('alpha::fs, 'beta::fs, 'gamma::fs) psi" 
+| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
 
 
 nominal_datatype 'a foo = 
-  Node x::"name" f::"('a::fs) foo" binds x in f
+  Node x::"name" f::"'a foo" binds x in f
 | Leaf "'a"
 
 term "Leaf"