diff -r 1c77e15c4259 -r f0252365936c Nominal/Ex/TypeVarsTest.thy --- a/Nominal/Ex/TypeVarsTest.thy Mon Nov 15 08:17:11 2010 +0000 +++ b/Nominal/Ex/TypeVarsTest.thy Mon Nov 15 09:52:29 2010 +0000 @@ -3,11 +3,13 @@ begin atom_decl name -declare [[STEPS = 100]] class s1 class s2 +instance nat :: s1 .. +instance int :: s2 .. + nominal_datatype ('a, 'b) lam = Var "name" | App "('a::s1, 'b::s2) lam" "('a, 'b) lam"