--- a/Nominal/Ex/Lambda.thy	Tue May 31 12:59:10 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue May 31 13:21:00 2011 +0900
@@ -100,9 +100,7 @@
   unfolding eqvt_def frees_lst_graph_def
   apply (rule, perm_simp, rule)
 apply(rule_tac y="x" in lam.exhaust)
-apply(simp_all)[3]
-apply(auto)[1]
-apply(simp_all)
+apply(auto)
 apply (erule Abs1_eq_fdest)
 apply(simp add: supp_removeAll fresh_def)
 apply(drule supp_eqvt_at)
@@ -111,9 +109,7 @@
 done
 
 termination
-  apply(relation "measure size")
-  apply(simp_all add: lam.size)
-  done
+  by (relation "measure size") (simp_all add: lam.size)
 
 text {* a small test lemma *}
 lemma
@@ -147,8 +143,7 @@
 done
 
 termination
-  by (relation "measure (\<lambda>(t,_,_). size t)")
-     (simp_all add: lam.size)
+  by (relation "measure (\<lambda>(t,_,_). size t)") (simp_all add: lam.size)
 
 lemma subst_eqvt[eqvt]:
   shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
@@ -511,6 +506,11 @@
   "map_term f (Var x) = f (Var x)"
 | "map_term f (App t1 t2) = App (f t1) (f t2)"
 | "map_term f (Lam [x].t) = Lam [x].(f t)"
+unfolding eqvt_def map_term_graph_def
+apply (rule, perm_simp, rule)
+apply (case_tac x, case_tac b rule: lam.exhaust)
+apply auto
+(*apply (erule Abs1_eq_fdest)*)
 oops
 
 nominal_primrec