--- a/CpsG.thy	Tue Dec 15 21:45:46 2015 +0800
+++ b/CpsG.thy	Tue Dec 15 15:10:40 2015 +0000
@@ -1842,6 +1842,7 @@
           Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" .
     also have "... = 
           Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)"
+  
     proof -
       from preced_kept have "the_preced s th2 = the_preced s' th2" by simp
       moreover have "cp_gen s ` RTree.children (tRAG s) x =
@@ -2000,7 +2001,6 @@
   by (insert eq_child_left[OF nd] eq_child_right, auto)
 
 lemma eq_cp:
-  fixes th' 
   assumes nd: "th \<notin> dependants s th'"
   shows "cp s th' = cp s' th'"
   apply (unfold cp_eq_cpreced cpreced_def)
@@ -2048,7 +2048,6 @@
 qed
 
 lemma eq_up:
-  fixes th' th''
   assumes dp1: "th \<in> dependants s th'"
   and dp2: "th' \<in> dependants s th''"
   and eq_cps: "cp s th' = cp s' th'"