diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Let.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -115,7 +115,7 @@
 | "height_trm (App l r) = max (height_trm l) (height_trm r)"
 | "height_trm (Lam v b) = 1 + (height_trm b)"
 | "height_trm (Let as b) = max (apply_assn height_trm as) (height_trm b)"
-  apply (simp only: eqvt_def height_trm_graph_def)
+  apply (simp only: eqvt_def height_trm_graph_aux_def)
   apply (rule, perm_simp, rule, rule TrueI)
   apply (case_tac x rule: trm_assn.exhaust(1))
   apply (auto)[4]
@@ -169,7 +169,7 @@
 | "subst s t (App l r) = App (subst s t l) (subst s t r)"
 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)"
 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (apply_assn2 (subst s t) as) (subst s t b)"
-  apply (simp only: eqvt_def subst_graph_def)
+  apply (simp only: eqvt_def subst_graph_aux_def)
   apply (rule, perm_simp, rule)
   apply (rule TrueI)
   apply (case_tac x)