--- a/Nominal/Ex/TypeVarsTest.thy	Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Wed Dec 22 09:13:25 2010 +0000
@@ -2,6 +2,13 @@
 imports "../Nominal2" 
 begin
 
+(* a nominal datatype with type variables and sorts *)
+
+
+(* the sort constraints need to be attached to the  *)
+(* first occurence of the type variables on the     *)
+(* left-hand side                                   *)
+
 atom_decl name
 
 class s1
@@ -10,14 +17,20 @@
 instance nat :: s1 ..
 instance int :: s2 .. 
 
-nominal_datatype ('a, 'b) lam =
+nominal_datatype ('a, 'b, 'c) lam =
   Var "name"
-| App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
-| Lam x::"name" l::"('a, 'b) lam"  bind x in l
+| App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam"
+| Lam x::"name" l::"('a, 'b, 'c) lam"  bind x in l
+| Foo "'a" "'b"
+| Bar x::"'c" l::"('a, 'b, 'c) lam"  bind x in l
+
+term Foo
+term Bar
 
 thm lam.distinct
 thm lam.induct
-thm lam.exhaust
+thm lam.exhaust 
+thm lam.strong_exhaust
 thm lam.fv_defs
 thm lam.bn_defs
 thm lam.perm_simps