# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1309239030 -32400
# Node ID 99069744ad7487308f7854dd7f785cb2260b3307
# Parent  13ae668bdb15dc99d3a45d1b807e61f206d230d4
Leftover only inj and eqvt

diff -r 13ae668bdb15 -r 99069744ad74 Nominal/Ex/LetRecB.thy
--- a/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:18:26 2011 +0900
+++ b/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:30:30 2011 +0900
@@ -159,14 +159,28 @@
   apply (simp add: eqvt_at_def height_trm_def)
   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 (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)
-  ...
+  apply (erule_tac c="()" in Abs_lst_fcb2)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: eqvt_at_def)
+  apply (simp add: eqvt_at_def)
+  defer defer
+  apply (subgoal_tac "(\<lambda>as x c. height_bp (fst (bp, b))) as x c = (\<lambda>as x c. height_bp (fst (bpa, ba))) as x c")
+  apply simp
+  apply (erule_tac c="()" in Abs_lst_fcb2)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: eqvt_at_def)
+  apply (simp add: eqvt_at_def)
+--""
   done
 
 termination by lexicographic_order