--- a/Tutorial/Lambda.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Tutorial/Lambda.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -38,7 +38,7 @@
   "height (Var x) = 1"
 | "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(simp add: eqvt_def height_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 using [[simproc del: alpha_lst]]
@@ -59,8 +59,8 @@
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
-  unfolding eqvt_def subst_graph_def
-  apply(rule, perm_simp, rule)
+  unfolding eqvt_def subst_graph_aux_def
+  apply(simp)
   apply(rule TrueI)
   using [[simproc del: alpha_lst]]
   apply(auto)