--- a/Tutorial/Lambda.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Tutorial/Lambda.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -39,7 +39,6 @@
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
 apply(simp add: eqvt_def height_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)
@@ -69,8 +68,10 @@
   apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(simp_all add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: perm_supp_eq fresh_star_Pair)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: perm_supp_eq fresh_star_Pair)
 done
 
 termination (eqvt)
@@ -82,7 +83,7 @@
   shows "atom z \<sharp> t[y ::= s]"
 using a b
 by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
-   (auto simp add: lam.fresh fresh_at_base)
+   (auto simp add: fresh_at_base)
 
 
 end