--- a/Nominal/Ex/Lambda.thy	Tue Jun 07 23:42:12 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue Jun 07 17:45:38 2011 +0100
@@ -436,7 +436,7 @@
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
-nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
+nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 where
   "trans (Var x) xs = lookup xs 0 x"
@@ -445,11 +445,13 @@
 apply(simp add: eqvt_def trans_graph_def)
 apply (rule, perm_simp, rule)
   apply (erule trans_graph.induct)
+  apply(simp)
   apply (case_tac "xa \<in> set xs")
   apply (simp add: fresh_star_def fresh_def supp_lookup_in)
   apply (simp add: fresh_star_def fresh_def supp_lookup_notin)
   apply blast
   apply (simp add: fresh_star_def ln.fresh)
+  apply(simp)
   apply (simp add: ln.fresh fresh_star_def)
 apply(case_tac x)
 apply(simp)