--- a/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:01:15 2011 +0900
+++ b/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:18:26 2011 +0900
@@ -160,19 +160,13 @@
   apply (simp add: eqvt_at_def height_bp_def)
   apply (simp add: eqvt_at_def height_bp_def)
   --"I'd like to apply FCB here, but the following fails"
-  apply (erule_tac c="()" and ba="bn" in Abs_lst_fcb2)
-
-  prefer 8
-  apply(assumption)
-  apply (drule_tac c="()" in Abs_lst_fcb2)
-  apply (simp add: Abs_eq_iff2)
-  apply (simp add: alphas)
-  apply clarify
-  apply (rule trans)
-  apply(rule_tac p="p" in supp_perm_eq[symmetric])
-  apply (simp add: pure_supp fresh_star_def)
-  apply (simp only: eqvts)
-  apply (simp add: eqvt_at_def)
+  apply (subgoal_tac "height_bp bp = height_bp bpa")
+  apply (subgoal_tac "height_trm b = height_trm ba")
+  apply simp
+  apply (subgoal_tac "(\<lambda>as x c. height_trm (snd (bp, b))) as x c = (\<lambda>as x c. height_trm (snd (bpa, ba))) as x c")
+  apply simp
+  apply (erule_tac c="()" and ba="bn" and f="\<lambda>as x c. height_trm (snd x)" in Abs_lst_fcb2)
+  ...
   done
 
 termination by lexicographic_order