# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1307465138 -3600
# Node ID c20a5e4027a4310f2861d1b9c53172e901e210cf
# Parent  a4d6689504e27ae7bd085178909769223763864a
merged

diff -r a4d6689504e2 -r c20a5e4027a4 Nominal/Ex/Lambda.thy
--- 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)