--- a/Nominal/Ex/Lambda.thy	Wed Apr 13 13:44:25 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Apr 18 15:56:07 2011 +0100
@@ -16,9 +16,19 @@
   Var: "triv (Var x) n"
 
 equivariance triv
-nominal_inductive triv avoids Var : "{}::name set"
-apply(auto simp add: fresh_star_def)
-done 
+nominal_inductive triv avoids Var: "{}::name set"
+apply(auto simp add: fresh_star_def) 
+done
+
+inductive 
+  triv2 :: "lam \<Rightarrow> nat \<Rightarrow> bool" 
+where
+  Var1: "triv2 (Var x) 0"
+| Var2: "triv2 (Var x) (n + n)"
+| Var3: "triv2 (Var x) n"
+
+equivariance triv2
+nominal_inductive triv2 .
 
 
 text {* height function *}