diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/LetRec.thy
--- a/Nominal/Ex/LetRec.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/LetRec.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -37,8 +37,8 @@
 | "height_trm (Lam v b) = 1 + (height_trm b)"
 | "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)"
 | "height_bp (Bp v t) = height_trm t"
-  apply (simp only: eqvt_def height_trm_height_bp_graph_def)
-  apply (rule, perm_simp, rule, rule TrueI)
+  apply (simp add: eqvt_def height_trm_height_bp_graph_aux_def)
+  apply(rule TrueI)
   using [[simproc del: alpha_set]]
   apply auto
   apply (case_tac x)