diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -17,9 +17,9 @@
 instance nat :: s1 ..
 instance int :: s2 .. 
 
-nominal_datatype ('a, 'b, 'c) lam =
+nominal_datatype ('a::"{s1,fs}", 'b::"{s2,fs}", 'c::at) lam =
   Var "name"
-| App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam"
+| App "('a, 'b, 'c) 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 *)
@@ -41,11 +41,11 @@
 
 nominal_datatype ('alpha, 'beta, 'gamma) psi =
   PsiNil
-| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
+| Output "'alpha::fs" "'alpha::fs" "('alpha::fs, 'beta::fs, 'gamma::fs) psi" 
 
 
 nominal_datatype 'a foo = 
-  Node x::"name" f::"'a foo" binds x in f
+  Node x::"name" f::"('a::fs) foo" binds x in f
 | Leaf "'a"
 
 term "Leaf"