--- a/Nominal/Ex/LetRec.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/LetRec.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -39,9 +39,11 @@
 | "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)
+  using [[simproc del: alpha_set]]
   apply auto
   apply (case_tac x)
   apply (case_tac a rule: let_rec.exhaust(1))
+  using [[simproc del: alpha_set]]
   apply auto
   apply (case_tac b rule: let_rec.exhaust(2))
   apply blast