--- 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"