--- a/Nominal/Ex/Lambda.thy	Tue May 24 19:39:38 2011 +0200
+++ b/Nominal/Ex/Lambda.thy	Wed May 25 21:38:50 2011 +0200
@@ -10,15 +10,17 @@
 | eVar nat
 
 inductive 
-  eval :: "expr \<Rightarrow> nat \<Rightarrow> bool"
+  eval :: "expr \<Rightarrow> nat list \<Rightarrow> bool"
 where
-  evCnst: "eval (eCnst c) 0"
-| evVar: "eval (eVar n) 2"
+  evCnst1: "eval (eCnst c) [2,1]"
+| evCnst2: "eval (eCnst b) [1,2]"
+| evVar: "eval (eVar n) [1]"
 
 inductive_cases 
-  evInv_Cnst: "eval (eCnst c) m"
+  evInv_Cnst: "eval (eCnst c) [1,2]"
 
-thm evInv_Cnst[simplified expr.distinct expr.eq_iff]
+thm evInv_Cnst
+
 
 
 atom_decl name
@@ -143,7 +145,8 @@
 defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
-apply(simp_all add: lam.distinct lam.eq_iff)
+apply(auto)[1]
+apply(simp_all)
 apply (erule Abs1_eq_fdest)
 apply(simp add: supp_removeAll fresh_def)
 apply(drule supp_eqvt_at)